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.

To generate verification conditions which can be loaded into HOL-Boogie, an additional Boogie plugin is required. See below for details.

Download

• Boogie plugin: Provers.Isabelle.dll (25. November 2009)
• Source code: hol-boogie-plugin.tar.gz (25. November 2009)

Requirements

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

Installation

Copy the plugin DLL into the directory where the Boogie executable resides.

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

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