Skip to main content

VeriSmall: Verified smallfoot shape analysis

Author(s): Appel, Andrew W.

To refer to this page use:
Abstract: We have implemented a version of the Smallfoot shape analyzer, calling upon a paramodulation-based heap theorem prover. Our implementation is done in Coq and is extractable to an efficient ML program. The program is verified correct in Coq with respect to our Separation Logic for C minor; this in turn is proved correct in Coq w.r.t. Leroy's operational semantics for C minor. Thus when our VeriSmall static analyzer claims some shape property of a program, an end-to-end machine-checked proof guarantees that the assembly language of the compiled program will actually have that property. © 2011 Springer-Verlag.
Publication Date: 28-Nov-2011
Citation: Appel, AW. "VeriSmall: Verified smallfoot shape analysis" Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7086 LNCS, 231 - 246, doi:10.1007/978-3-642-25379-9_18
DOI: doi:10.1007/978-3-642-25379-9_18
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 231 - 246
Type of Material: Conference Article
Series/Report no.: Lecture Notes in Computer Science;
Journal/Proceeding Title: First International Conference, December 7-9, 2011, Kenting, Taiwan.
Version: This is the author’s final manuscript. All rights reserved to author(s).

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.