HOL-Boogie
From MaRDI portal
swMATH409MaRDI QIDQ13169FDOQ13169
Author name not available (Why is that?)
Official website: http://www.springerlink.com/content/w171805777015235/fulltext.pdf
Cited In (23)
- Extending Sledgehammer with SMT solvers
- Inferring Loop Invariants Using Postconditions
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- A framework for the verification of certifying computations
- IMP++
- HOL-Z
- distcc
- Omnibus
- Traffic 4
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- BoogiePL
- Graph Theory
- Maximum Cardinality Matching
- Robbins Conjecture
- ShortestPath
- Verification and code generation for invariant diagrams in Isabelle
- Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Extending Sledgehammer with SMT solvers
- Proving fairness and implementation correctness of a microkernel scheduler
- A dynamic logic for unstructured programs with embedded assertions
- Title not available (Why is that?)
This page was built for software: HOL-Boogie
