Skip to Main content Skip to Navigation
Conference papers

Congruence Closure with Free Variables

Haniel Barbosa 1, 2, 3 Pascal Fontaine 1, 3 Andrew Reynolds 4
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Wednesday, September 20, 2017 - 2:23:28 PM
Last modification on : Wednesday, November 3, 2021 - 4:49:36 AM


Files produced by the author(s)




Haniel Barbosa, Pascal Fontaine, Andrew Reynolds. Congruence Closure with Free Variables. TACAS 2017 - 23rd International Conference on Tools and Algorithms for Construction and Analysis of Systems, Apr 2017, Uppsala, Sweden. pp.220 - 230, ⟨10.1007/10721959_17⟩. ⟨hal-01590918⟩



Les métriques sont temporairement indisponibles