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
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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
Liste complète des métadonnées

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-00642544
Contributor : Pascal Fontaine <>
Submitted on : Wednesday, March 7, 2012 - 3:21:57 PM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM
Document(s) archivé(s) le : Friday, November 23, 2012 - 4:00:34 PM

File

paper3.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00642544, version 1

Citation

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⟩

Share

Metrics

Record views

4403

Files downloads

185