A Flexible Proof Format for SMT: a Proposal

Frédéric Besson 1 Pascal Fontaine 2, 3 Laurent Théry 4
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 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.
Type de document :
Communication dans un congrès
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011, 〈http://pxtp2011.loria.fr〉
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00642544
Contributeur : Pascal Fontaine <>
Soumis le : mercredi 7 mars 2012 - 15:21:57
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 23 novembre 2012 - 16:00:34

Fichier

paper3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00642544, version 1

Citation

Frédéric Besson, Pascal Fontaine, Laurent Théry. A Flexible Proof Format for SMT: a Proposal. Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011, 〈http://pxtp2011.loria.fr〉. 〈hal-00642544〉

Partager

Métriques

Consultations de la notice

3302

Téléchargements de fichiers

158