Boogie is a program verification condition generator for an imperative core language. It has front-ends for the programming languages C# and C enriched by annotations in first-order logic. Its verification conditions - constructed via a wp calculus from these annotations - are usually transferred to automated theorem provers such as Simplify or Z3. In this paper, however, we present a proof-environment, HOL-BoogieP, that combines Boogie with the interactive theorem prover Isabelle/HOL. In particular, we present specific techniques combining automated and interactive proof methods for code-verification. We will exploit our proof-environment in two ways: First, we present scenarios to "debug" annotations (in particular: invariants) by interactive proofs. Second, we use our environment also to verify "background theories", i.e. theories for data-types used in annotations as well as memory and machine models underlying the verification method for C. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Böhme, S., Leino, K. R. M., & Wolff, B. (2008). HOL-Boogie - An interactive prover for the boogie program-verifier. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 150–166). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_15
Mendeley helps you to discover research relevant for your work.