Top

Published in:

2017 | OriginalPaper | Chapter

Congruence Closure with Free Variables

Authors : Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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 \(\mathsf{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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter HiFrog: SMT-based Function Summarization for Software Verification

next chapter On Optimization Modulo Theories, MaxSMT and Sorting Networks

It is assumed, without loss of generality, that \({\mathbf {T}}({E\cup L})\) contains at least one ground term of each sort in \({E\cup L}\).

For CCFV to generate such solutions it is sufficient to add the side condition to Assign that s is a variable or a ground term and to remove the side condition of U_var. This will lead to the application of U_var in each

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54580-5_13/447563_1_En_13_IEq229_HTML.gif

Currently the ground congruence closure procedures are not closed under entailment w.r.t. disequalities. E.g. \(g(f(a), h(b))\not \simeq g(f(b), h(a))\in E\) does not lead to the addition of \(a\not \simeq b\) to the data structure. A complete implementation of CCFV requires the ground congruence closure to entail all entailed disequalities.

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)CrossRefMATH

Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A., (eds) Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press (2001)

Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217–247 (1994)MathSciNetCrossRefMATH

Backeman, P., Rümmer, P.: Efficient algorithms for bounded rigid E-unification. In: Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 70–85. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24312-2_6 CrossRef

Backeman, P., Rümmer, P.: Theorem proving with bounded rigid E-unification. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 572–587. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21401-6_39 CrossRef

Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. Technical report, Inria (2016). https://hal.inria.fr/hal-01442691

Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14 CrossRef

Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)

Barrett, C., Stump, A., Tinelli, C.: The SML-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds) International Workshop on Satisfiability Modulo Theories (SMT) (2010)

10.

Beckert, B.: Ridig E-unification. In: Bibel, W., Schimidt, P.H. (eds.) Automated Deduction: A Basis for Applications. Foundations: Calculi and Methods, vol. 1. Kluwer Academic Publishers, Dordrecht (1998)

11.

Bouton, T., de Oliveira, D.C.B., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_12 CrossRef

12.

de Moura, L., Bjørner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73595-3_13 CrossRef

13.

de Moura, L., Bjørner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475–490. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71070-7_40 CrossRef

14.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24 CrossRef

15.

Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 611–706. Elsevier, Amsterdam (2001)CrossRef

16.

Déharbe, D., Fontaine, P., Le Berre, D., Mazure, B.: Computing prime implicants. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 46–52. IEEE (2013)

17.

Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)MathSciNetCrossRefMATH

18.

Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, New York (1990)CrossRefMATH

19.

Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_25 CrossRef

20.

Goubault, J.: A rule-based algorithm for rigid E-unification. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1993. LNCS, vol. 713, pp. 202–210. Springer, Heidelberg (1993). doi:10.1007/BFb0022569 CrossRef

21.

Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)MathSciNetCrossRefMATH

22.

Nieuwenhuis, R., Oliveras, A.: Fast congruence closure, extensions. Inf. Comput. 205(4), 557–580 (2007). Special Issue: 16th International Conference on Rewriting Techniques and ApplicationsMathSciNetCrossRefMATH

23.

Piskac, R., Wies, T., Zufferey, D.: GRASShopper - complete heap verification with mixed specifications. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124–139. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_9 CrossRef

24.

Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 195–202. FMCAD Inc (2014)

25.

Reynolds, A., Tinelli, C., Goel, A., Krstić, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 377–391. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_26 CrossRef

26.

Rümmer, P.: E-matching with free variables. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 359–374. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28717-6_28 CrossRef

27.

Tiwari, A., Bachmair, L., Ruess, H.: Rigid E-unification revisited. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 220–234. Springer, Heidelberg (2000). doi:10.1007/10721959_17 CrossRef

Title: Congruence Closure with Free Variables
Authors: Haniel Barbosa
Pascal Fontaine
Andrew Reynolds
Publisher: Springer Berlin Heidelberg
Book: Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-662-54579-9

Electronic ISBN: 978-3-662-54580-5

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-662-54580-5_13

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner