HOL-Boogie -- an interactive prover-backend for the verifying C compiler
From MaRDI portal
Publication:2655335
DOI10.1007/s10817-009-9142-9zbMath1185.68211OpenAlexW2100855196WikidataQ122198171 ScholiaQ122198171MaRDI QIDQ2655335
Wolfram Schulte, Michał Moskal, Burkhart Wolff, Sascha Böhme
Publication date: 25 January 2010
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-009-9142-9
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Verification and code generation for invariant diagrams in Isabelle ⋮ Extending Sledgehammer with SMT Solvers ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ A framework for the verification of certifying computations ⋮ Extending Sledgehammer with SMT solvers
Uses Software
Cites Work
- Proving fairness and implementation correctness of a microkernel scheduler
- Balancing the load. Leveraging a semantics stack for systems verification
- Verifying a signature architecture: a comparative case study
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Isabelle/HOL. A proof assistant for higher-order logic
- Generating error traces from verification-condition counterexamples
- Types, bytes, and separation logic
- Building Formal Method Tools in the Isabelle/Isar Framework
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Simplify: a theorem prover for program checking
- The specification statement
- Computer Aided Verification
- Logic for Programming, Artificial Intelligence, and Reasoning
- Tools and Algorithms for the Construction and Analysis of Systems
This page was built for publication: HOL-Boogie -- an interactive prover-backend for the verifying C compiler
