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