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 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
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. Giorgino, Mathieu; Strecker, Martin: Correctness of pointer manipulating algorithms illustrated by a verified BDD construction (2012)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  6. Böhme, Sascha; Fox, Anthony C. J.; Sewell, Thomas; Weber, Tjark: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL (2011)
  7. Ulbrich, Mattias: A dynamic logic for unstructured programs with embedded assertions (2011)
  8. Beckert, Bernhard; Moskal, Michal: Deductive verification of system software in the verisoft XT project (2010) ioport
  9. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  10. Furia, Carlo Alberto; Meyer, Bertrand: Inferring loop invariants using postconditions (2010)
  11. James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
  12. Daum, Matthias; Dörrenbächer, Jan; Wolff, Burkhart: Proving fairness and implementation correctness of a microkernel scheduler (2009)
  13. Böhme, Sascha; Leino, K. Rustan M.; Wolff, Burkhart: HOL-Boogie -- an interactive prover for the Boogie program-verifier (2008)
  14. Brucker, Achim D.; Wolff, Burkhart: An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (2008)