Lazy Proofs for DPLL(T)-Based SMT Solvers

by Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean
Abstract:
With the integration of SMT solvers into analysis frameworks aimed at ensuring a system’s end-to-end correctness, having a high level of confidence in these solvers’ results has become crucial. For unsatisfiable queries, a reasonable approach is to have the solver return an independently checkable proof of unsatisfiability. We propose a lazy, extensible and robust method for enhancing DPLL(T)-style SMT solvers with proof-generation capabilities. Our method maintains separate Boolean-level and theory-level proofs, and weaves them together into one coherent artifact. Each theory-specific solver is called upon lazily, a posteriori, to prove precisely those solution steps it is responsible for and that are needed for the final proof. We present an implementation of our technique in the CVC4 SMT solver. CVC4 can produce unsatisfiability proofs for quantifier-free queries involving uninterpreted functions, arrays, bitvectors and combinations thereof. We discuss an evaluation of our tool using industrial benchmarks and benchmarks from the SMT-LIB library, which shows promising results.
Reference:
Lazy Proofs for DPLL(T)-Based SMT Solvers (Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean), In Proceedings of the 16th International Conference on Formal Methods In Computer-Aided Design (FMCAD ’16) (Ruzica Piskac, Muralidhar Talupur, eds.), FMCAD Inc., 2016. (Mountain View, CA. Best paper award.)
Bibtex Entry:
@inproceedings{KBT+16,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/KBT+16.pdf",
  author    = "Guy Katz and Clark Barrett and Cesare Tinelli and Andrew Reynolds and Liana Hadarean",
  title     = "Lazy Proofs for {DPLL(T)}-Based {SMT} Solvers",
  booktitle = "Proceedings of the 16th International Conference on Formal Methods In Computer-Aided Design (FMCAD '16)",
  editor    = "Ruzica Piskac and Muralidhar Talupur",
  publisher = "FMCAD Inc.",
  pages     = "93--100",
  month     = oct,
  year      = 2016,
  note      = "Mountain View, CA.  {Best paper award.}",
  category  = "Conference Publications",
  abstract  = "With the integration of SMT solvers into analysis
  frameworks aimed at ensuring a system's end-to-end
  correctness, having a high level of confidence in
  these solvers' results has become crucial. For unsatisfiable queries,
  a reasonable approach is to have the solver
  return an independently checkable proof of unsatisfiability.
  We propose a lazy, extensible and robust method for enhancing
  DPLL(T)-style SMT solvers with proof-generation capabilities. Our method
  maintains separate Boolean-level and theory-level proofs, and
  weaves them together into one coherent artifact. Each
  theory-specific solver is called upon lazily, a posteriori, to prove precisely
  those solution steps it is responsible for and that are needed for the final proof.
  We present an implementation of our technique in the CVC4 SMT solver.
  CVC4 can produce unsatisfiability proofs for quantifier-free queries involving
  uninterpreted functions, arrays, bitvectors and combinations thereof. 
  We discuss an evaluation of our tool using industrial benchmarks and benchmarks 
  from the SMT-LIB library, which shows promising results."
}

Fork me on GitHub