Bridging the Gap: Automatic Verified Abstraction of C

Select |




Print


Greenaway, David; Andronick, June; Klein, Gerwin

Greenaway, David; Andronick, June; Klein, Gerwin


2012-08-12


Conference Material


Interactive Theorem Proving 2012


Princeton, New Jersey, USA


99-115


Before low-level imperative code can be reasoned about in an interactive theorem prover, it must first be converted into a logical representation in that theorem prover. Accurate translations of such code should be conservative, choosing safe representations over representations convenient to reason about. This paper bridges the gap between conservative representation and convenient reasoning. We present a tool that automatically abstracts low-level C semantics into higher level specifications, while generating proofs of refinement in Isabelle/HOL for each translation step. The aim is to generate a verified, human-readable specification, convenient for further reasoning.


Springer Berlin / Heidelberg


C Verification, Abstraction, Refinement


https://doi.org/10.1007/978-3-642-32347-8_8


http://itp2012.cs.princeton.edu/


The final publication is available at www.springerlink.com


nicta:5662


Greenaway, David; Andronick, June; Klein, Gerwin. Bridging the Gap: Automatic Verified Abstraction of C. In: Lennart Beringer and Amy Felty Editor, editor/s. Interactive Theorem Proving 2012; Princeton, New Jersey, USA. Springer Berlin / Heidelberg; 2012-08-12. 99-115. https://doi.org/10.1007/978-3-642-32347-8_8



Loading citation data...

Citation counts
(Requires subscription to view)