HOL-Boogie

HOL-Boogie is an interactive back-end for the Boogie program verifier and, in particular, may be used to proof verification conditions arising from C programs. HOL-Boogie is contained in the theorem prover Isabelle/HOL. For more information, see this article or this article, or contact me.

Requirements

• Isabelle2009-1
• Boogie: version 2
• optionally: VCC

Usage of the HOL-Boogie Plugin

For generating a HOL-Boogie exchange file (to be loaded in Isabelle), execute the following command-line:

boogie /prover:Isabelle /proverOpt:ISABELLE_INPUT=NAME.b2i NAME.bpl

or, when using VCC:

vcc /b:/prover:Isabelle /b:/proverOpt:ISABELLE_INPUT=NAME.b2i NAME.c