HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier

DOI10.1007/978-3-540-71067-7_15MaRDI QIDQ3543656zbMATH OpenOpenAlexFDO

Authors Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_15

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Verifying Whiley programs with Boogie
• Logic for Programming, Artificial Intelligence, and Reasoning
• Imperative Functional Programming with Isabelle/HOL
• Why3 -- where programs meet provers

Cites work

• Building Formal Method Tools in the Isabelle/Isar Framework
• Generating error traces from verification-condition counterexamples
• Logic for Programming, Artificial Intelligence, and Reasoning
• The specification statement
• Verifying a signature architecture: a comparative case study

Cited in

(14)

• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• HOL-Boogie
• A framework for the verification of certifying computations
• Faster and more complete extended static checking for the Java modeling language
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• A dynamic logic for unstructured programs with embedded assertions
• Inferring Loop Invariants Using Postconditions
• scientific article; zbMATH DE number 7649972 (Why is no real title available?)
• The HOL-CSP Refinement Toolkit
• Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
• Priority Search Trees
• HOL-CSP Version 2.0
• A Sound Type System for Physical Quantities, Units, and Measurements
• Proving fairness and implementation correctness of a microkernel scheduler

Describes a project that uses

Uses Software

• SMT-LIB
• Why3
• ESC/Java
• Isabelle/HOL
• Spec#
• SIMPLIFY
• Boogie
• KRAKATOA
• Caduceus
• z3
• BoogiePL

This page was built for publication: HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543656)