HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler

HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler

Typ: Seminarthema Betreuer: Mattias Ulbrich

Links: Paper

Boogie is a verification condition generator for an imperative core language and has front-ends for many programming languages. Boogie’s verification conditions are usually transferred to automated theorem provers. In this paper, a proof environment, HOL-Boogie, that combines Boogie with the interactive theorem prover Isabelle/HOL is presented. In particular, the authors Böhme, Moskal, Schulte, and Wolff present specific techniques combining automated and interactive proof methods for code verification. The main goal of the environment is to help program verification engineers in their task to "debug" annotations and to find combined proofs where purely automatic proof attempts fail.