Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
From MaRDI portal
Publication:3100212
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
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
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