VeriSmall: Verified smallfoot shape analysis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationCertified Programs and Proofs - First International Conference, CPP 2011, Proceedings
Pages231-246
Number of pages16
DOIs
StatePublished - Nov 28 2011
Event1st International Conference on Certified Programs and Proofs, CPP 2011 - Kenting, Taiwan, Province of China
Duration: Dec 7 2011Dec 9 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7086 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other1st International Conference on Certified Programs and Proofs, CPP 2011
CountryTaiwan, Province of China
CityKenting
Period12/7/1112/9/11

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'VeriSmall: Verified smallfoot shape analysis'. Together they form a unique fingerprint.

Cite this