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.68225MaRDI QIDQ3100212
A. C. J. Fox, Tjark Weber, Sascha Böhme, Thomas D. Sewell
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
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item