VeriSmall: Verified smallfoot shape analysis

Appel, Andrew W.

VeriSmall: Verified smallfoot shape analysis

Author(s): Appel, Andrew W.

Download

To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1fg60

Full metadata record

DC Field	Value	Language
dc.contributor.author	Appel, Andrew W.	-
dc.date.accessioned	2016-10-17T14:13:44Z	-
dc.date.available	2016-10-17T14:13:44Z	-
dc.date.issued	2011-11-28	en_US
dc.identifier.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	en_US
dc.identifier.issn	0302-9743	-
dc.identifier.uri	http://arks.princeton.edu/ark:/88435/pr1fg60	-
dc.description.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.	en_US
dc.format.extent	231 - 246	en_US
dc.relation.ispartof	First International Conference, December 7-9, 2011, Kenting, Taiwan.	en_US
dc.relation.ispartofseries	Lecture Notes in Computer Science;	-
dc.rights	This is the author’s final manuscript. All rights reserved to author(s).	en_US
dc.title	VeriSmall: Verified smallfoot shape analysis	en_US
dc.type	Conference Article	en_US
dc.identifier.doi	doi:10.1007/978-3-642-25379-9_18	-
dc.identifier.eissn	1611-3349	-

Files in This Item:

File	Description	Size	Format
AppelCPP2011.pdf		191.34 kB	Adobe PDF	View/Download

Show Simple Item Record