Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
Authors:
- 1 January 2011
- book chapter
- Published by Springer Nature
- p. 183-198
Abstract
No abstract availableKeywords
This publication has 24 references indexed in Scilit:
- LCF-Style Bit-Blasting in HOL42011
- Compression of Propositional Resolution Proofs via Partial Regularization2011
- Extending Sledgehammer with SMT Solvers2011
- Fast LCF-Style Proof Reconstruction for Z32010
- Isabelle Theories for Machine WordsElectronic Notes in Theoretical Computer Science, 2009
- HOL-Boogie—An Interactive Prover-Backend for the Verifying C CompilerJournal of Automated Reasoning, 2009
- Data Compression for Proof ReplayJournal of Automated Reasoning, 2008
- A Short Presentation of Coq2008
- CVC32007
- Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants2006