Alethe: Towards a Generic SMT Proof Format (extended abstract)
Hans-J\"org Schurr (University of Lorraine, CNRS, Inria, and LORIA),, Mathias Fleury (Johannes Kepler University Linz), Haniel Barbosa, (Universidade Federal de Minas Gerais), Pascal Fontaine (University of, Li\`ege)
TL;DR
This paper reviews the evolution of the Alethe proof format for SMT solvers, discusses its current state, and seeks community feedback to guide future enhancements and address potential issues.
Contribution
It provides a comprehensive overview of the Alethe format's development, its adoption in multiple solvers, and proposes a pragmatic approach for future improvements.
Findings
The format has matured over ten years.
Multiple solvers now generate proofs in this format.
Community feedback is sought for future development.
Abstract
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that might arise when other solvers use the format.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.