HOL-Boogie
From MaRDI portal
Software:13169
swMATH409MaRDI QIDQ13169FDOQ13169
Author name not available (Why is that?)
Cited In (13)
- 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 Dynamic Logic for Unstructured Programs with Embedded Assertions
- A framework for the verification of certifying computations
- Extending Sledgehammer with SMT Solvers
- 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
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
- Title not available (Why is that?)
This page was built for software: HOL-Boogie
