haRVey: combining reasoners

David Déharbe 1 Pascal Fontaine 2
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present the architecture of the oncoming version of the SMT (Satisfiability Modulo Theories) solver haRVey. haRVey checks the satisfiability of a formula written in a first-order language with interpreted symbols from various theories. Its new architecture is original, first in the sense that it is a combination of reasoners, rather than the traditional combination of decision procedures. Second, one of these reasoners is a full-featured first-order saturation-based prover. Finally, some of those reasoners in the combination may only be sporadically activated not using computer time when inactive. We believe those new features will contribute to the efficiency and expressivity of the new version of the tool.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.152-156, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

https://hal.inria.fr/inria-00091662
Contributeur : Stephan Merz <>
Soumis le : mercredi 6 septembre 2006 - 19:14:28
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 10:21:04

Fichier

Identifiants

  • HAL Id : inria-00091662, version 1

Collections

Citation

David Déharbe, Pascal Fontaine. haRVey: combining reasoners. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.152-156, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00091662〉

Partager

Métriques

Consultations de la notice

144

Téléchargements de fichiers

121