Paper Info
Title
Lazy proofs for DPLL(T)-based SMT solvers.
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, capable of producing 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.
Year
DOI
Venue
2016
10.1109/FMCAD.2016.7886666
FMCAD
Keywords
Field
DocType
lazy proofs,DPLL(T)-based SMT solvers,system end-to-end correctness,unsatisfiable queries,checkable proof,proof-generation capabilities,Boolean-level proofs,theory-level proofs,CVC4 SMT solver,unsatisfiability proofs,quantifier-free queries,uninterpreted functions,bitvectors,SMT-LIB library
Digital electronics,Programming language,Computer science,Correctness,A priori and a posteriori,Theoretical computer science,DPLL algorithm,Mathematical proof,Solver,Benchmark (computing),Satisfiability modulo theories
Conference
ISBN
Citations 
PageRank 
978-1-5386-2692-4
1
0.35
References 
Authors
11
5
Name
Order
Citations
PageRank
Guy Katz126117.17
Clark Barrett21268108.65
Cesare Tinelli3140979.86
Andrew Reynolds421214.79
Liana Hadarean5663.57