haRVey: combining reasoners - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

haRVey: combining reasoners

Résumé

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.
Fichier principal
Vignette du fichier
avocs.pdf (99.72 Ko) Télécharger le fichier

Dates et versions

inria-00091662 , version 1 (06-09-2006)

Identifiants

  • HAL Id : inria-00091662 , version 1

Citer

David Déharbe, Pascal Fontaine. haRVey: combining reasoners. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.152-156. ⟨inria-00091662⟩
68 Consultations
159 Téléchargements

Partager

Gmail Facebook X LinkedIn More