“Flexible Proof Production in an Industrial-Strength SMT Solver” by Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark Barrett. In Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), (Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, eds.), Aug. 2022, pp. 15-35.
Proof production for SMT solvers is paramount to ensure their correctness independently from implementations, which are often prohibitively difficult to verify. Historically, however, SMT proof production has struggled with performance and coverage issues, resulting in the disabling of many crucial solving techniques and in coarse-grained (and thus hard to check) proofs. We present a flexible proof-production architecture designed to handle the complexity of versatile, industrial-strength SMT solvers and show how we leverage it to produce detailed proofs, including for components previously unsupported by any solver. The architecture allows proofs to be produced modularly, lazily, and with numerous safeguards for correctness. This architecture has been implemented in the state-of-the-art SMT solver cvc5. We evaluate its proofs for SMT-LIB benchmarks and show that the new architecture produces better coverage than previous approaches, has acceptable performance overhead, and supports detailed proofs for most solving components.
BibTeX entry:
@inproceedings{BRK+22,
author = {Haniel Barbosa and Andrew Reynolds and Gereon Kremer and
Hanna Lachnitt and Aina Niemetz and Andres N{\"o}tzli and Alex
Ozdemir and Mathias Preiner and Arjun Viswanathan and Scott Viteri
and Yoni Zohar and Cesare Tinelli and Clark Barrett},
editor = {Jasmin Blanchette and Laura Kov{\'a}cs and Dirk Pattinson},
title = {Flexible Proof Production in an Industrial-Strength SMT Solver},
booktitle = {Proceedings of the {\it 11^{th}} International Joint
Conference on Automated Reasoning (IJCAR '22)},
series = {Lecture Notes in Computer Science},
volume = {13385},
pages = {15--35},
publisher = {Springer Nature},
month = aug,
year = {2022},
doi = {10.1007/978-3-031-10769-6_3},
url = {http://theory.stanford.edu/~barrett/pubs/BRK+22.pdf}
}
(This webpage was created with bibtex2web.)