Lazy proofs for DPLL(T)-based SMT solvers
Lazy proofs for DPLL(T)-based SMT solvers
复制标题
基于 DPLL(T) 的 SMT 求解器的惰性证明
DOI：
10.1109/fmcad.2016.7886666
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Liana Hadarean
中科院分区：
文献类型：
--
作者：
Guy Katz;Clark W. Barrett;C. Tinelli;Andrew Reynolds;Liana Hadarean
随着SMT求解器集成到旨在确保系统端到端正确性的分析框架中，对这些求解器的结果具有高度的信心变得至关重要。对于不可满足的查询，一个合理的方法是让求解器返回一个可独立检查的不可满足性证明。我们提出了一个懒惰的，可扩展的和强大的方法，以增强DPLL（T）风格的SMT求解器与证明生成能力。我们的方法维护单独的布尔级和理论级证明，并将它们编织在一起成为一个连贯的工件。每个特定于理论的求解器都被懒惰地、后验地调用，以精确地证明它所负责的以及最终证明所需的那些求解步骤。我们提出了一个实现我们的技术在CVC 4 SMT求解器，能够产生不可满足性证明的量化器的自由查询涉及未解释的功能，数组，位向量及其组合。我们讨论了我们的工具使用工业基准和基准从SMT-LIB库，这表明了可喜的成果的评估。
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.
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson