HOL-Boogie
From MaRDI portal
Software:13169
No author found.
Related Items (13)
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 ⋮ Verification and code generation for invariant diagrams in Isabelle ⋮ Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction ⋮ Inferring Loop Invariants Using Postconditions ⋮ Extending Sledgehammer with SMT Solvers ⋮ A Dynamic Logic for Unstructured Programs with Embedded Assertions ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ An extensible encoding of object-oriented data models in HOL. With an application to IMP++ ⋮ A framework for the verification of certifying computations ⋮ Extending Sledgehammer with SMT solvers
This page was built for software: HOL-Boogie
