Trustworthy Systems

Bridging the gap: Automatic verified abstraction of C

Authors

David Greenaway, June Andronick and Gerwin Klein

UNSW

Abstract

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

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

Download