Email Gateway (Aug 18 2022 at 13:49): Email Gateway (Aug 18 2022 at 13:49):From: Sascha Boehme <boehmes@in.tum.de>
We are pleased to announce the online version of the following JAR article:
HOL-Boogie --- An Interactive Prover-Backend for the Verified C Compiler
DOI: 10.1007/s10817-009-9142-9
Link: http://www.springerlink.com/content/a62734x4l74x563x/
Abstract:
Boogie is a verification condition generator for an imperative core language.
It has front-ends for the programming languages C# and C enriched by
annotations in first-order logic, i.e. pre- and postconditions, assertions, and
loop invariants. Moreover, concepts like ghost fields, ghost variables, ghost
code and specification functions have been introduced to support a specific
modeling methodology. Boogie's verification conditions --- constructed via a wp
calculus from annotated programs --- are usually transferred to automated theorem provers such as Simplify or Z3. This also comprises the expansion of
language-specific modeling constructs in terms of a theory describing memory
and elementary operations on it; this theory is called machine/memory model. In
this paper, we present a proof environment, HOL-Boogie, that combines Boogie
with the interactive theorem prover Isabelle/HOL, for a specific C front-end
and machine/memory model. In particular, we present specific techniques
combining automated and interactive proof methods for code verification. The
main goal of our environment is to help program verification engineers in their
task to 'debug' annotations and to find combined proofs where purely automatic
proof attempts fail.
Sascha Böhme
Michal Moskał
Wolfram Schulte
Burkhart Wolff
Last updated: May 03 2024 at 01:09 UTC