Fine-grained SMT Proofs for the Theory of Fixed-width Bit-vectors

by Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters
Abstract:
Many high-level verification tools rely on SMT solvers to efficiently discharge complex verification conditions. Some applications require more than just a yes/no answer from the solver. For satisfiable quantifier-free problems, a satisfying assignment is a natural artifact. In the unsatisfiable case, an externally checkable proof can serve as a certificate of correctness and can be mined to gain additional insight into the problem. We present a method of encoding and checking SMT-generated proofs for the quantifier-free theory of fixed-width bitvectors. Proof generation and checking for this theory poses several challenges, especially for proofs based on reductions to propositional logic. Such reductions can result in large resolution subproofs in addition to requiring a proof that the reduction itself is correct. We describe a fine-grained proof system formalized in the LFSC framework that addresses some of these challenges with the use of computational side-conditions. We report results using a proof-producing version of the CVC4 SMT solver on unsatisfiable quantifier-free bit-vector benchmarks from the SMT-LIB benchmark library.
Reference:
Fine-grained SMT Proofs for the Theory of Fixed-width Bit-vectors (Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters), In Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR ’15) (Martin Davis, Ansgar Fehnker, Annabelle McIver, Andrei Voronkov, eds.), Springer, volume 9450, 2015. (Suva, Fiji)
Bibtex Entry:
@inproceedings{HBR+15,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/HBR+.pdf",
  author    = "Liana Hadarean and Clark Barrett and Andrew Reynolds and Cesare Tinelli and Morgan Deters",
  title     = "Fine-grained {SMT} Proofs for the Theory of Fixed-width Bit-vectors",
  booktitle = "Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '15)",
  series    = "Lecture Notes in Computer Science",
  publisher = "Springer",
  volume    = 9450,
  editor    = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov},
  pages     = "340--355",
  month     = nov,
  year      = 2015,
  note      = "Suva, Fiji",
  category  = "Conference Publications",
  abstract  = "Many high-level verification tools rely on SMT solvers to efficiently
discharge complex verification conditions. Some applications require more than
just a yes/no answer from the solver. For satisfiable quantifier-free problems, a
satisfying assignment is a natural artifact. In the unsatisfiable case, an externally
checkable proof can serve as a certificate of correctness and can be mined to
gain additional insight into the problem. We present a method of encoding and
checking SMT-generated proofs for the quantifier-free theory of fixed-width bitvectors.
Proof generation and checking for this theory poses several challenges,
especially for proofs based on reductions to propositional logic. Such reductions
can result in large resolution subproofs in addition to requiring a proof that the
reduction itself is correct. We describe a fine-grained proof system formalized
in the LFSC framework that addresses some of these challenges with the use of
computational side-conditions. We report results using a proof-producing version
of the CVC4 SMT solver on unsatisfiable quantifier-free bit-vector benchmarks
from the SMT-LIB benchmark library."
}

Fork me on GitHub