Abstract
The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent reconstruction of unsatisfiability proofs for bit-vector theories in the theorem provers HOL4 and Isabelle/HOL. Our work shows that LCF-style proof reconstruction for the theory of fixed-size bit-vectors, although difficult because Z3's proofs provide limited detail, is often possible. We thereby obtain high correctness assurances for Z3's results, and increase the degree of proof automation for bit-vector problems in HOL4 and Isabelle/HOL. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Böhme, S., Fox, A. C. J., Sewell, T., & Weber, T. (2011). Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7086 LNCS, pp. 183–198). https://doi.org/10.1007/978-3-642-25379-9_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
