HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
From MaRDI portal
Publication:3543656
DOI10.1007/978-3-540-71067-7_15zbMath1165.68399OpenAlexW1515169568MaRDI QIDQ3543656
Burkhart Wolff, Sascha Böhme, K. Rustan M. Leino
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
Related Items
Proving fairness and implementation correctness of a microkernel scheduler, Faster and more complete extended static checking for the Java modeling language, HOL-Boogie -- an interactive prover-backend for the verifying C compiler, Unnamed Item, Inferring Loop Invariants Using Postconditions, A Dynamic Logic for Unstructured Programs with Embedded Assertions, HOL-Boogie, An extensible encoding of object-oriented data models in HOL. With an application to IMP++, A framework for the verification of certifying computations
Uses Software
Cites Work
