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.


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
Last updated: 25.11.2009