Abstract:


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


Sascha Böhme and Rustan Leino and Burkhart Wolff



Boogie is a program verification condition generator 
for animperative core language. It has front-ends for 
the programming languagesC# 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 proverssuch as Simplify or Z3. In this paper, 
however, we present a proof-environment,HOL-Boogie, 
that combines Boogie with the interactivetheorem 
prover Isabelle/HOL. In particular, we present specific 
techniquescombining automated and interactive proof 
methods for code-verification.We will exploit our 
proof-environment in two ways: First, we present 
scenariosto &duml;ebug" annotations (in particular: 
invariants) by interactiveproofs. Second, we use our 
environment also to verify &buml;ackground theories",
i.e. theories for data-types used in annotations as 
well as memoryand machine models underlying the 
verification method for C.