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

Sascha Böhme, Anthony Fox, Thomas Sewell, and Tjark Weber. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 183-198. Springer, 2011.

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.

Download

The original publication is available at www.springerlink.com.

BibTeX

@inproceedings{boehme11reconstruction,
  author    = {Sascha B{\"o}hme and Anthony Fox and Thomas Sewell and Tjark Weber},
  title     = {Reconstruction of {Z3}'s Bit-Vector Proofs in {HOL4} and {Isabelle/HOL}},
  editor    = {Jean-Pierre Jouannaud and Zhong Shao},
  booktitle = {Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December~7-9, 2011. Proceedings},
  volume    = {7086},
  series    = {Lecture Notes in Computer Science},
  pages     = {183--198},
  publisher = {Springer},
  year      = {2011},
  url       = {http://dx.doi.org/10.1007/978-3-642-25379-9_15}
}

Benchmarks

Benchmarks and detailed evaluation data are available here.
Last modified: 2014-05-06