Combining decision procedures by (model-)equality propagation. (English) Zbl 1243.68150
Summary: Formal methods in software and hardware design often generate formulas that need to be validated, either interactively or automatically. Among the automatic tools, SMT (satisfiability modulo theories) solvers are particularly suitable to discharge such proof obligations, as their input language is equational logic with symbols from various useful decidable fragments such as uninterpreted symbols, linear arithmetic, and usual data-structures like arrays or lists. In this paper, we present an approach to combine decision procedures and propositional solvers into an SMT-solver, based not only on the exchange of deducible equalities between decision procedures, but also on the generation of model equalities by decision procedures. This extends nicely the classical Nelson-Oppen combination procedure in a simple platform to smoothly combine convex and non-convex theories. We show the soundness and completeness of this approach using an original abstract framework to represent and reason about SMT-solvers. We then describe an algorithmic translation of this method, implemented in the kernel of the veriT solver.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B70 | Logic in computer science |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
formal verification; automated theorem proving; SMT solving; combination of decision proceduresReferences:
| [1] | M. Abadi, L. Lamport, The existence of refinement mappings. Technical Report 29, 1988, DEC/SRC. · Zbl 0728.68083 |
| [2] | Abrial, J. -R.: The B-book: assigning programs to meanings, (1996) · Zbl 0915.68015 |
| [3] | Baaz, M.; Egly, U.; Leitsch, A.: Normal form transformations, Handbook of automated reasoning. Vol. I, 273-333 (2001) · Zbl 1005.03013 |
| [4] | Barrett, C.; Deters, M.; Oliveras, A.; Stump, A.: Design and results of the 3rd annual satisfiability modulo theories competition (SMT-COMP 2007), International journal on artificial intelligence tools 17, No. 4, 569-606 (2008) |
| [5] | Barrett, C.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C.: Splitting on demand in SAT modulo theories, Lecture notes in computer science 4246, 512-526 (2006) · Zbl 1165.68480 · doi:10.1007/11916277_35 |
| [6] | Barrett, C.; Sebastiani, R.; Seshia, S. A.; Tinelli, C.: Satisfiability modulo theories, Frontiers in artificial intelligence and applications 185, 825-885 (2009) |
| [7] | Barrett, C. W.; Dill, D. L.; Stump, A.: A generalization of shostak’s method for combining decision procedures, Lecture notes in computer science 2309, 132-146 (2002) · Zbl 1057.68109 |
| [8] | Barsotti, D.; Nieto, L. P.; Tiu, A.: Verification of clock synchronization algorithms: experiments on a combination of deductive tools, Formal aspects of computing 19, No. 3, 321-341 (2007) · Zbl 1125.68107 · doi:10.1007/s00165-007-0027-6 |
| [9] | Bouton, T.; De Oliveira, D. C. B.; Déharbe, D.; Fontaine, P.: Verit: an open, trustable and efficient SMT-solver, Lecture notes in computer science 5663, 151-156 (2009) |
| [10] | Bruttomesso, R.; Cimatti, A.; Franzén, A.; Griggio, A.; Sebastiani, R.: Delayed theory combination vs. Nelson–oppen for satisfiability modulo theories: a comparative analysis, Lecture notes in computer science 4246, 527-541 (2006) · Zbl 1165.68483 · doi:10.1007/11916277_36 |
| [11] | Cornélio, M.; Cavalcanti, A.; Sampaio, A.: Refactoring towards a layered architecture, Proc. Brazilian symposium on formal methods, SBMF 2004, 199-216 (2004) · Zbl 1272.68092 |
| [12] | Davis, M.; Logemann, G.; Loveland, D.: A machine program for theorem proving, Communications of the ACM 5, No. 7, 394-397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557 |
| [13] | De Moura, L.; Bjørner, N.: Model-based theory combination, Electronic notes in theoretical computer science 198, No. 2, 37-49 (2008) · Zbl 1277.03007 |
| [14] | De Moura, L.; Bjørner, N.: Z3: an efficient SMT solver, Lecture notes in computer science 4963, 337-340 (2008) |
| [15] | De Oliveira, D. C. B.; Déharbe, D.; Fontaine, P.: Combining decision procedures by (model-)equality propagation, Electronic notes in theoretical computer science 240, 113-128 (2009) · Zbl 1347.68309 |
| [16] | Eén, N.; Sörensson, N.: An extensible SAT-solver, Lecture notes in computer science 2919, 333-336 (2003) |
| [17] | Fontaine, P.; Gribomont, E. P.: Combining non-stably infinite, non-first order theories, Electronic notes in theoretical computer science 125, 37-51 (2005) · Zbl 1272.68355 |
| [18] | Fontaine, P.; Marion, J. -Y.; Merz, S.; Nieto, L. P.; Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants, Lecture notes in computer science 3920, 167-181 (2006) · Zbl 1180.68240 · doi:10.1007/11691372 |
| [19] | , Introduction to HOL: A theorem proving environment for higher order logic (1993) · Zbl 0779.68007 |
| [20] | Harrison, J.: HOL light: a tutorial introduction, Lecture notes in computer science 1166, 265-269 (1996) |
| [21] | G. Huet, G. Kahn, C. Paulin-Mohring, The Coq Proof Assistant – a tutorial, 2004, Version 8.0. |
| [22] | Lahiri, S. K.; Musuvathi, M.: An efficient decision procedure for UTVPI constraints, Lecture notes in computer science 3717, 168-183 (2005) · Zbl 1171.68715 · doi:10.1007/11559306 |
| [23] | Lahiri, S. K.; Musuvathi, M.: An efficient Nelson–oppen decision procedure for difference constraints over rationals, Electronic notes in theoretical computer science 144, No. 2, 27-41 (2006) · Zbl 1272.68360 |
| [24] | Leino, K. R. M.: Object invariants in specification and verification, Proc. Brazilian symposium on formal methods, SBMF 2006, 3-4 (2006) |
| [25] | Morgan, C.: Programming from specifications, (1994) · Zbl 0829.68083 |
| [26] | Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S.: Chaff: engineering an efficient SAT solver, , 530-535 (2001) |
| [27] | Nelson, G.; Oppen, D.: Simplification by cooperating decision procedures, ACM transactions on programming languages and systems 1, No. 2, 245-257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079 |
| [28] | Nelson, G.; Oppen, D.: Fast decision procedures based on congruence closure, Journal of the ACM 27, No. 2, 356-364 (1980) · Zbl 0441.68111 · doi:10.1145/322186.322198 |
| [29] | Nieuwenhuis, R.; Oliveras, A.: \(DPLL(T)\) with exhaustive theory propagation and its application to difference logic, Lecture notes in computer science 3576, 321-334 (2005) · Zbl 1081.68629 · doi:10.1007/b138445 |
| [30] | Nipkow, T.; Paulson, L.; Wenzel, M.: Isabelle/HOL, Lecture notes in computer science 2283 (2002) · Zbl 0994.68131 |
| [31] | Nonnengart, A.; Weidenbach, C.: Computing small clause normal forms, Handbook of automated reasoning. Vol. I, 335-367 (2001) · Zbl 0992.03018 |
| [32] | Oppen, D. C.: Complexity, convexity and combinations of theories, Theoretical computer science 12, No. 3, 291-302 (1980) · Zbl 0437.03007 · doi:10.1016/0304-3975(80)90059-6 |
| [33] | V. Pratt, Two easy theories whose combination is hard, 1977. http://citeseer.ist.psu.edu/pratt77two.html. |
| [34] | S. Ranise, C. Tinelli, The SMT-LIB standard: Version 1.2, 2006. |
| [35] | Shostak, R. E.: Deciding combinations of theories, Journal of the ACM 31, No. 1, 1-12 (1984) · Zbl 0629.68089 · doi:10.1145/2422.322411 |
| [36] | Tinelli, C.; Harandi, M. T.: A new correctness proof of the Nelson–oppen combination procedure, Proc. frontiers of combining systems, frocos. Applied logic, 103-120 (1996) · Zbl 0893.03001 |
| [37] | Tinelli, C.; Zarba, C. G.: Combining nonstably infinite theories, Journal of automated reasoning 34, No. 3, 209-238 (2005) · Zbl 1108.03014 · doi:10.1007/s10817-005-5204-9 |
| [38] | Zhang, L.; Madigan, C.; Moskewicz, M.; Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver, , 279-285 (2001) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
