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.
@inproceedings{Greenaway_AK_12,
title = {Bridging the Gap: Automatic Verified Abstraction of {C}},
author = {David Greenaway and June Andronick and Gerwin Klein},
booktitle = {Proceedings of the 3rd International Conference on
Interactive Theorem Proving},
year = {2012},
month = {aug},
volume = {7406},
pages = {99--115},
address = {Princeton, New Jersey},
editor = {Lennart Beringer and Amy Felty},
publisher = {Springer},
isbn = {978-3-642-32346-1},
series = {Lecture Notes in Computer Science}
}