Skip to Main content Skip to Navigation
Conference papers

Alethe: Towards a Generic SMT Proof Format (extended abstract)

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03341413
Contributor : Hans-Jörg Schurr Connect in order to contact the contributor
Submitted on : Friday, September 10, 2021 - 5:25:41 PM
Last modification on : Friday, February 4, 2022 - 1:43:51 PM

File

pxtp2021.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine. Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP 2021 - 7th Workshop on Proof eXchange for Theorem Proving, Sep 2021, Pittsburgh, PA / virtual, United States. pp.49-54, ⟨10.4204/EPTCS.336.6⟩. ⟨hal-03341413⟩

Share

Metrics

Record views

60

Files downloads

62