Combining Decision Procedures by (Model-)Equality Propagation

Abstract : 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.
Type de document :
Article dans une revue
Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of the Eleventh Brazilian Symposium on Formal Methods (SBMF 2008), 240 (2), pp.113-128. 〈10.1016/j.entcs.2009.05.048〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00430636
Contributeur : Pascal Fontaine <>
Soumis le : lundi 9 novembre 2009 - 13:02:38
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Lien texte intégral

Identifiants

Collections

Citation

Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. Combining Decision Procedures by (Model-)Equality Propagation. Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of the Eleventh Brazilian Symposium on Formal Methods (SBMF 2008), 240 (2), pp.113-128. 〈10.1016/j.entcs.2009.05.048〉. 〈inria-00430636〉

Partager

Métriques

Consultations de la notice

77