HOL-Boogie

MaRDI QIDQ13169swMATHFDO

Official website http://www.springerlink.com/content/w171805777015235/fulltext.pdf

Described by source

• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier

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