## HOL-Boogie — An Interactive Prover-Backend for the Verifying C Compiler

Sascha Böhme, Michał Moskal, Wolfram Schulte, and Burkhart Wolff

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 a 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 a 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.

Bibtex entry:

@article{ author = {Sascha B{\"o}hme and Micha{\l} Moskal and Wolfram Schulte and Burkhart Wolff}, title = {{HOL-Boogie} --- {An} Interactive Prover-Backend for the {Verifying} {C} {Compiler}}, journal = {Journal of Automated Reasoning}, volume = 44, number = {1--2}, pages = {111--144}, month = feb, year = 2010, doi = {http://dx.doi.org/10.1007/s10817-009-9142-9}, }