HOL-Boogie—An Interactive Prover for the Boogie Program-Verifier
Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff
Abstract:
Boogie is a program 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.
Its verification conditions — constructed via a wp calculus from
these annotations — are usually transferred to automated theorem
provers such as Simplify or Z3. In this paper, however, we present a
proof-environment, HOL-Boogie, that combines Boogie with the
interactive theorem prover Isabelle/HOL. In particular, we present
specific techniques combining automated and interactive proof methods
for code-verification.
We will exploit our proof-environment in two ways: First, we present
scenarios to "debug" annotations (in particular: invariants)
by interactive proofs. Second, we use our environment also to verify
"background theories", i.e. theories for data-types used in
annotations as well as memory and machine models underlying the
verification method for C.
Bibtex entry:
@inproceedings{ author = {Sascha B{\"o}hme and K. Rustan M. Leino and Burkhart Wolff}, title = {{HOL-Boogie}---{An} Interactive Prover for the {Boogie} Program-Verifier}, booktitle = {Theorem Proving in Higher Order Logics}, editor = {Otmane Ait Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar}, series = {Lecture Notes in Computer Science}, volume = {5170}, year = 2008, pages = {150--166}, publisher = {Springer}, doi = {http://dx.doi.org/10.1007/978-3-540-71067-7_15} }