Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL

DOI10.1007/978-3-642-25379-9_15zbMath1350.68225OpenAlexW197756383MaRDI QIDQ3100212

A. C. J. Fox, Thomas D. Sewell, Sascha Böhme, Tjark Weber

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_15

Mathematics Subject Classification ID

Related Items

The reflective Milawa theorem prover is sound (down to the machine code that runs it), CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver, Scalable fine-grained proofs for formula processing, Deciding Bit-Vector Formulas with mcSAT, Flexible proof production in an industrial-strength SMT solver, Extending Sledgehammer with SMT solvers

Uses Software

• HOL-Boogie
• ML
• Isabelle/HOL
• SMT-LIB
• cvc3
• z3
• HOL
• SATzilla
• HOL Light
• Sledgehammer
• CVC Lite

Cites Work

• Unnamed Item
• Unnamed Item
• Efficiently checking propositional refutations in HOL theorem provers
• Data compression for proof replay
• Edinburgh LCF. A mechanized logic of computation
• Efficiently solving quantified bit-vector formulas
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• LCF-Style Bit-Blasting in HOL4
• A Short Presentation of Coq
• Constructive Type Classes in Isabelle
• Extending Sledgehammer with SMT Solvers
• Compression of Propositional Resolution Proofs via Partial Regularization
• Theorem Proving in Higher Order Logics
• Fast LCF-Style Proof Reconstruction for Z3
• Tools and Algorithms for the Construction and Analysis of Systems