Lazy proofs for DPLL(T)-based SMT solvers

By Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean. 2016

35 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Clark W. Barrett
2. Guy Katz
3. David L. Dill
4. Mykel J. Kochenderfer
5. Kyle D. Julian
6. Cesare Tinelli
7. Andrew Reynolds
8. Aina Niemetz

In Computational Theory and Mathematics

1. Clark W. Barrett
2. Guy Katz
3. David L. Dill
4. Mykel J. Kochenderfer
5. Cesare Tinelli
6. Kyle D. Julian
7. Andrew Reynolds
8. Aina Niemetz

In Computer Networks and Communications

1. Clark W. Barrett
2. Guy Katz
3. Andrew Reynolds
4. David L. Dill
5. Cesare Tinelli
6. Tim King

Citations in the corpus

• Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017, background): “Another direction is to provide better soundness guarantees without harming performance, for example by replaying floating-point solutions using precise arithmetic [17], or by producing externally-checkable correctness proofs [15].”
• cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “The Proof Module of cvc5 was built from scratch and replaces the proof system of CVC4 [67, 77], which was incomplete and suffered from a number of architectural shortcomings.”