×

Efficient interpolant generation in satisfiability modulo theories. (English) Zbl 1134.68402

Ramakrishnan, C. R. (ed.) et al., Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-78799-0/pbk). Lecture Notes in Computer Science 4963, 397-412 (2008).
Summary: The problem of computing Craig Interpolants for propositional (SAT) formulas has recently received a lot of interest, mainly for its applications in formal verification. However, propositional logic is often not expressive enough for representing many interesting verification problems, which can be more naturally addressed in the framework of Satisfiability Modulo Theories, SMT.
Although some works have addressed the topic of generating interpolants in SMT, the techniques and tools that are currently available have some limitations, and their performace still does not exploit the full power of current state-of-the-art SMT solvers.
In this paper we try to close this gap. We present several techniques for interpolant generation in SMT which overcome the limitations of the current generators mentioned above, and which take full advantage of state-of-the-art SMT technology. These novel techniques can lead to substantial performance improvements wrt. the currently available tools.
We support our claims with an extensive experimental evaluation of our implementation of the proposed techniques in the MathSAT SMT solver.
For the entire collection see [Zbl 1133.68009].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

FOCI; Zap
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying industrial hybrid systems with mathsat. Electr. Notes Theor. Comput. Sci. 119(2) (2005) · Zbl 1272.68220
[2] Audemard, G.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R.; Peled, D. A.; Vardi, M. Y., Bounded model checking for timed systems, Formal Techniques for Networked and Distributed Systems - FORTE 2002 (2002), Heidelberg: Springer, Heidelberg · Zbl 1037.68549 · doi:10.1007/3-540-36135-9_16
[3] Ball, T.; Lahiri, S. K.; Musuvathi, M.; Sutcliffe, G.; Voronkov, A., Zap: Automated theorem proving for software analysis, Logic for Programming, Artificial Intelligence, and Reasoning (2005), Heidelberg: Springer, Heidelberg · Zbl 1143.68576 · doi:10.1007/11591191_2
[4] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: A Tight Integration of SAT and Mathematical Decision Procedure. Journal of Automated Reasoning 35(1-3) (October 2005) · Zbl 1109.68101
[5] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient Theory Combination via Boolean Search. Information and Computation 204(10) (2006) · Zbl 1137.68578
[6] Bruttomesso, R.; Cimatti, A.; Franzén, A.; Griggio, A.; Sebastiani, R.; Hermann, M.; Voronkov, A., Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis, Logic for Programming, Artificial Intelligence, and Reasoning (2006), Heidelberg: Springer, Heidelberg · Zbl 1165.68483
[7] Cabodi, G.; Murciano, M.; Nocco, S.; Quer, S., Stepping forward with interpolants in unbounded model checking, Proc. ICCAD 2006 (2006), New York: ACM, New York
[8] Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. Technical Report DIT-07-075, DISI - University of Trento (2007) · Zbl 1134.68402
[9] Cotton, S.; Maler, O.; Biere, A.; Gomes, C. P., Fast and Flexible Difference Constraint Propagation for DPLL(T), Theory and Applications of Satisfiability Testing - SAT 2006, 170-183 (2006), Heidelberg: Springer, Heidelberg · Zbl 1187.68537 · doi:10.1007/11814948_19
[10] Dutertre, B.; de Moura, L.; Ball, T.; Jones, R. B., A Fast Linear-Arithmetic Solver for DPLL(T), Computer Aided Verification, 81-94 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11817963_11
[11] Henzinger, T. A.; Jhala, R.; Majumdar, R.; McMillan, K. L.; Jones, N. D.; Leroy, X., Abstractions from proofs, POPL (2004), New York: ACM, New York · Zbl 1325.68147
[12] Jhala, R.; McMillan, K.; Etessami, K.; Rajamani, S. K., Interpolant-based transition relation approximation, Computer Aided Verification, 39-51 (2005), Heidelberg: Springer, Heidelberg · Zbl 1081.68622
[13] Jhala, R.; McMillan, K. L.; Hermanns, H.; Palsberg, J., A Practical and Complete Approach to Predicate Refinement, Tools and Algorithms for the Construction and Analysis of Systems (2006), Heidelberg: Springer, Heidelberg · Zbl 1180.68118 · doi:10.1007/11691372_33
[14] Jhala, R.; McMillan, K. L.; Damm, W.; Hermanns, H., Array Abstractions from Proofs, Computer Aided Verification (2007), Heidelberg: Springer, Heidelberg · Zbl 1135.68474 · doi:10.1007/978-3-540-73368-3_23
[15] Kapur, D.; Majumdar, R.; Zarba, C. G.; Young, M.; Devanbu, P. T., Interpolation for data structures, SIGSOFT FSE (2006), New York: ACM, New York
[16] Kroening, D.; Weissenbacher, G., Lifting Propositional Interpolants to the Word-Level, FMCAD, 85-89 (2007), Los Alamitos, CA, USA: IEEE Computer Society, Los Alamitos, CA, USA
[17] Li, B.; Somenzi, F.; Hermanns, H.; Palsberg, J., Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking, Tools and Algorithms for the Construction and Analysis of Systems, 227-241 (2006), Heidelberg: Springer, Heidelberg · Zbl 1180.68176 · doi:10.1007/11691372_15
[18] Marques-Silva, J., Interpolant Learning and Reuse in SAT-Based Model Checking, Electr. Notes Theor. Comput. Sci., 174, 3, 31-43 (2007) · Zbl 1277.68140 · doi:10.1016/j.entcs.2006.12.021
[19] McMillan, K.: Interpolation and SAT-based model checking. In: Proc. CAV (2003) · Zbl 1278.68184
[20] McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1) (2005) · Zbl 1079.68092
[21] McMillan, K. L.; Ball, T.; Jones, R. B., Lazy Abstraction with Interpolants, Computer Aided Verification, 123-136 (2006), Heidelberg: Springer, Heidelberg · Zbl 1188.68196 · doi:10.1007/11817963_14
[22] Nelson, G., Oppen, D.: Simplification by Cooperating Decision Procedures. ACM Trans. on Programming Languages and Systems 1(2) (1979) · Zbl 0452.68013
[23] Nieuwenhuis, R.; Oliveras, A.; Etessami, K.; Rajamani, S. K., DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic, Computer Aided Verification (2005), Heidelberg: Springer, Heidelberg
[24] Nieuwenhuis, R.; Oliveras, A., Fast Congruence Closure and Extensions, Inf. Comput., 2005, 4, 557-580 (2007) · Zbl 1112.68116 · doi:10.1016/j.ic.2006.08.009
[25] Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. of Symb. Logic 62(3) (1997) · Zbl 0945.03086
[26] Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2006), http://www.SMT-LIB.org
[27] Rybalchenko, A.; Sofronie-Stokkermans, V., Constraint Solving for Interpolation, VMCAI (2007), Heidelberg: Springer, Heidelberg · Zbl 1132.68480
[28] Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, J.SAT 3 (2007) · Zbl 1145.68501
[29] Vanderbei, R. J., Linear Programming: Foundations and Extensions (2001), Heidelberg: Springer, Heidelberg · Zbl 1043.90002
[30] Yorsh, G.; Musuvathi, M.; Nieuwenhuis, R., A combination method for generating interpolants, Automated Deduction - CADE-20, 353-368 (2005), Heidelberg: Springer, Heidelberg · Zbl 1135.03331
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.