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)

• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• IMP++
• HOL-Z
• Omnibus
• distcc
• A framework for the verification of certifying computations
• Extending Sledgehammer with SMT solvers
• Traffic 4
• 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
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• BoogiePL
• Inferring Loop Invariants Using Postconditions
• Graph Theory
• Robbins Conjecture
• Maximum Cardinality Matching
• ShortestPath
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Verification and code generation for invariant diagrams in Isabelle
• Extending Sledgehammer with SMT solvers
• scientific article; zbMATH DE number 7649972 (Why is no real title available?)
• Proving fairness and implementation correctness of a microkernel scheduler

This page was built for software: HOL-Boogie