GridTPT: a distributed platform for Theorem Prover Testing

Thomas Bouton 1 Diego Caminha B. de Oliveira 1 David Déharbe 2 Pascal Fontaine 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 UFRN - Universidade Federal do Rio Grande do Norte [Natal]
Abstract : Programming provers is a complex task; completeness or even soundness may often be broken by apparently harmless bugs. A good testing platform can contribute in detecting problems early and helping development. This paper presents the distributed platform for testing the veriT SMT solver. Its features are fairly standard, but it allows to easily distribute the task in a cluster. We plan to distribute this platform as an open source tool for the community of developers of automated theorem provers. This presentation to PAAR2010 would provide the opportunity to discuss the need for such a tool and the necessary features in a broader context. We would like to extract a requirement specification from this discussion, that would be useful to get dedicated implementation resources for distribution, maintenance and future development of the tool.
Type de document :
Communication dans un congrès
2nd Workshop on Practical Aspects of Automated Reasoning (PAAR), Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées
https://hal.inria.fr/inria-00543805
Contributeur : Pascal Fontaine <>
Soumis le : lundi 6 décembre 2010 - 16:39:35
Dernière modification le : mardi 24 avril 2018 - 13:34:57

Identifiants

  • HAL Id : inria-00543805, version 1

Collections

INRIA | GRID5000 | LORIA | UNIV-LORRAINE

Citation

Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. GridTPT: a distributed platform for Theorem Prover Testing. 2nd Workshop on Practical Aspects of Automated Reasoning (PAAR), Jul 2010, Edinburgh, United Kingdom. 2010. 〈inria-00543805〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

93

Contact


archive-ouverte@inria.fr