Combining Decision Procedures by (Model-)Equality Propagation

Diego Caminha B. De Oliveira; David Déharbe; Pascal Fontaine

inria-00430636, version 1

Combining Decision Procedures by (Model-)Equality Propagation

Diego Caminha B. De Oliveira ¹, David Déharbe ², Pascal Fontaine () ¹

Electronic Notes in Theoretical Computer Science 240, 2 (2009) 113-128

Résumé : SMT (Satisfiability Modulo Theories) solvers are automatic verification engines suitable to discharge important classes of proof obligations generated in applying formal construction of software and hardware designs. In this paper, we present a new approach to combine decision procedures and propositional solvers into an SMT-solver. This approach is based on the generation of model equalities by decision procedures. We show the soundness and completeness of the proposed approach using an original abstract framework to represent and reason about SMT-solvers. We then present an algorithmic version of the new SMT-solving approach and discuss practical aspects of our implementation.

1 : MOSEL (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2 : Universidade Federal de Rio Grande do Norte (UFRN)
Universidade Federal de Rio Grande do Norte

inria-00430636, version 1
http://hal.inria.fr/inria-00430636
oai:hal.inria.fr:inria-00430636
Contributeur : Pascal Fontaine <>
Soumis le : Lundi 9 Novembre 2009, 13:02:38
Dernière modification le : Lundi 4 Avril 2011, 12:03:13

Voir la fiche détaillée

Documents associés

DOI : 10.1016/j.entcs.2009.05.048

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="article"><head>Articles dans des revues avec comité de lecture</head>
<biblStruct type="article" xml:id="inria-00430636"><analytic>
<author><persName><forename>Diego</forename><surname>Caminha B. De Oliveira</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>David</forename><surname>Déharbe</surname></persName>
<affiliation>
<orgName type="laboratory">UFRN</orgName>
<orgName type="team">Universidade Federal de Rio Grande do Norte</orgName>
<country>BR</country>
<orgName type="institution">Universidade Federal de Rio Grande do Norte</orgName>
</affiliation>
</author>
<author><persName><forename>Pascal</forename><surname>Fontaine</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">Combining Decision Procedures by (Model-)Equality Propagation</title></analytic><monogr><title level="j" type="main">Electronic Notes in Theoretical Computer Science</title><imprint><publisher>Elsevier</publisher><biblScope type="publicationDate">2009-00-00</biblScope><biblScope type="vol">240</biblScope><biblScope type="issue">2</biblScope><biblScope type="pp">113-128</biblScope></imprint></monogr><idno type="doi">10.1016/j.entcs.2009.05.048</idno><idno type="HALid">http://hal.inria.fr/inria-00430636</idno></biblStruct>
</listBibl>
</listBibl>