Alethe: Towards a Generic SMT Proof Format (extended abstract) - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

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

Résumé

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.
Fichier principal
Vignette du fichier
pxtp2021.pdf (152.82 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03341413 , version 1 (10-09-2021)

Identifiants

Citer

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⟩
88 Consultations
99 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More