Skip to main content

Bridging the gap: Automatic verified abstraction of C


David Greenaway, June Andronick and Gerwin Klein



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.

BibTeX Entry

    author           = {Greenaway, David and Andronick, June and Klein, Gerwin},
    doi              = {10.1007/978-3-642-32347-8_8},
    editor           = {{Lennart Beringer and Amy Felty}},
    month            = aug,
    year             = {2012},
    keywords         = {c verification, abstraction, refinement},
    address          = {Princeton, New Jersey, USA},
    title            = {Bridging the Gap: Automatic Verified Abstraction of {C}},
    pages            = {99--115},
    booktitle        = {International Conference on Interactive Theorem Proving},
    publisher        = {Springer}


Served by Apache on Linux on seL4.