Skip to Main content Skip to Navigation
Conference papers

A Flexible Proof Format for SMT: a Proposal

Frédéric Besson 1 Pascal Fontaine 2 Laurent Théry 3
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
2 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
3 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The standard input format for Satisfiability Modulo Theories (SMT) solvers has now reached its second version and integrates many of the features useful for users to interact with their favourite SMT solver. However, although many SMT solvers do output proofs, no standardised proof format exists. We, here, propose for discussion at the PxTP Workshop a generic proof format in the SMT-LIB philosophy that is flexible enough to be easily recast for any SMT solver. The format is configurable so that the proof can be provided by the solver at the desired level of detail.
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Wednesday, March 7, 2012 - 3:21:57 PM
Last modification on : Tuesday, October 19, 2021 - 11:58:52 PM
Long-term archiving on: : Friday, November 23, 2012 - 4:00:34 PM


Files produced by the author(s)


  • HAL Id : hal-00642544, version 1


Frédéric Besson, Pascal Fontaine, Laurent Théry. A Flexible Proof Format for SMT: a Proposal. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. ⟨hal-00642544⟩



Record views


Files downloads