HOL-Boogie—An Interactive Prover for the Boogie Program-Verifier

Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff

Document: PDF, slides

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}
}