Conference proceeding
Flexible Proof Production in an Industrial-Strength SMT Solver
AUTOMATED REASONING, IJCAR 2022, Vol.13385, pp.15-35
Lecture Notes in Artificial Intelligence
01/01/2022
DOI: 10.1007/978-3-031-10769-6_3
Abstract
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.
Details
- Title: Subtitle
- Flexible Proof Production in an Industrial-Strength SMT Solver
- Creators
- Haniel Barbosa - Universidade Federal de Minas GeraisAndrew Reynolds - University of IowaGereon Kremer - Stanford UniversityHanna Lachnitt - Stanford UniversityAina Niemetz - Stanford UniversityAndres Notzli - Stanford UniversityAlex Ozdemir - Stanford UniversityMathias Preiner - Stanford UniversityArjun Viswanathan - University of IowaScott Viteri - Stanford UniversityYoni Zohar - Bar-Ilan UniversityCesare Tinelli - University of IowaClark Barrett - Stanford University
- Contributors
- J Blanchette (Editor)L Kovacs (Editor)D Pattinson (Editor)
- Resource Type
- Conference proceeding
- Publication Details
- AUTOMATED REASONING, IJCAR 2022, Vol.13385, pp.15-35
- Series
- Lecture Notes in Artificial Intelligence
- DOI
- 10.1007/978-3-031-10769-6_3
- ISSN
- 0302-9743
- eISSN
- 1611-3349
- Publisher
- Springer Nature
- Number of pages
- 21
- Grant note
- 68335-17-C-0558 / Office of Naval Research 2110397; 2020704 / NSF-BSF
- Language
- English
- Date published
- 01/01/2022
- Academic Unit
- Computer Science
- Record Identifier
- 9984410853602771
Metrics
34 Record Views