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.\parIts 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.\parWe 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.

References in zbMATH (referenced in 13 articles , 1 standard article )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Preoteasa, Viorel; Back, Ralph-Johan; Eriksson, Johannes: Verification and code generation for invariant diagrams in Isabelle (2015)
  2. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  3. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  4. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  5. Böhme, Sascha; Fox, Anthony C.J.; Sewell, Thomas; Weber, Tjark: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL (2011)
  6. Ulbrich, Mattias: A dynamic logic for unstructured programs with embedded assertions (2011)
  7. Beckert, Bernhard; Moskal, Michal: Deductive verification of system software in the verisoft XT project (2010) ioport
  8. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  9. Furia, Carlo Alberto; Meyer, Bertrand: Inferring loop invariants using postconditions (2010)
  10. James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
  11. Daum, Matthias; Dörrenbächer, Jan; Wolff, Burkhart: Proving fairness and implementation correctness of a microkernel scheduler (2009)
  12. Böhme, Sascha; Leino, K.Rustan M.; Wolff, Burkhart: HOL-Boogie -- an interactive prover for the Boogie program-verifier (2008)
  13. Brucker, Achim D.; Wolff, Burkhart: An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (2008)