Cited in
(23)- Inferring Loop Invariants Using Postconditions
- Extending Sledgehammer with SMT solvers
- 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
- BoogiePL
- Graph Theory
- Maximum Cardinality Matching
- Robbins Conjecture
- ShortestPath
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Verification and code generation for invariant diagrams in Isabelle
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Extending Sledgehammer with SMT solvers
- Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
- Proving fairness and implementation correctness of a microkernel scheduler
- A dynamic logic for unstructured programs with embedded assertions
- scientific article; zbMATH DE number 7649972 (Why is no real title available?)
This page was built for software: HOL-Boogie
