Congruence Closure with Free Variables

Abstract : Many verification techniques nowadays successfully rely on SMT solvers as back-ends to automatically discharge proof obligations. These solvers generally rely on various instantiation techniques to handle quantifiers. We here show that the major instantiation techniques in SMT solving can be cast in a unifying framework for handling quantified formulas with equality and uninterpreted functions. This framework is based on the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a sound and complete calculus to solve this problem in practice: Congruence Closure with Free Variables (CCFV). Experimental evaluations of implementations of CCFV in the state-of-the-art solver CVC4 and in the solver veriT exhibit improvements in the former and makes the latter competitive with state-of-the-art solvers in several benchmark libraries stemming from verification efforts.
Type de document :
Rapport
[Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017
Liste complète des métadonnées

https://hal.inria.fr/hal-01442691
Contributeur : Haniel Barbosa <>
Soumis le : lundi 23 janvier 2017 - 19:20:56
Dernière modification le : vendredi 15 décembre 2017 - 21:29:43
Document(s) archivé(s) le : lundi 24 avril 2017 - 15:31:34

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01442691, version 2

Collections

Citation

Haniel Barbosa, Pascal Fontaine, Andrew Reynolds. Congruence Closure with Free Variables. [Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017. 〈hal-01442691v2〉

Partager

Métriques

Consultations de la notice

178

Téléchargements de fichiers

47