Constraint solving for interpolation. (English) Zbl 1213.68389
Summary: Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing the separation between the sets of ‘good’ and ‘bad’ states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in a black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Beyer, D.; Zufferey, D.; Majumdar, R., CSIsat: interpolation for LA+EUF, (Computer Aided Verification, 20th International Conference, CAV 2008. Proceedings. Computer Aided Verification, 20th International Conference, CAV 2008. Proceedings, LNCS, vol. 5123 (2008)), 304-308 |
| [2] | Bradley, A. R.; Manna, Z.; Sipma, H. B., Linear ranking with reachability, (CAV’2005: Computer Aided Verification. CAV’2005: Computer Aided Verification, LNCS, vol. 3576 (2005), Springer), 491-504 · Zbl 1081.68611 |
| [3] | Cimatti, A.; Griggio, A.; Sebastiani, R., Efficient interpolant generation in satisfiability modulo theories, (Ramakrishnan, C. R.; Rehof, J., 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. 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, LNCS, vol. 4963 (2008)), 397-412 · Zbl 1134.68402 |
| [4] | Cimatti, A.; Griggio, A.; Sebastiani, R., Interpolant generation for UTVPI, (Schmidt, R. A., Automated Deduction — CADE-22, 22nd International Conference on Automated Deduction. Proceedings. Automated Deduction — CADE-22, 22nd International Conference on Automated Deduction. Proceedings, LNCS, vol. 5663 (2009)), 167-182 · Zbl 1250.68186 |
| [5] | Colón, M.; Sankaranarayanan, S.; Sipma, H., Linear invariant generation using non-linear constraint solving, (CAV’2003: Computer Aided Verification. CAV’2003: Computer Aided Verification, LNCS, vol. 2725 (2003), Springer), 420-432 · Zbl 1278.68164 |
| [6] | Cousot, P., Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming, (VMCAI’2005: Verification, Model Checking, and Abstract Interpretation. VMCAI’2005: Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 3385 (2005), Springer), 1-24 · Zbl 1111.68503 |
| [7] | Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, Journal of Symbolic Logic, 22, 3, 250-268 (1957) · Zbl 0081.24402 |
| [8] | Esparza, J.; Kiefer, S.; Schwoon, S., Abstraction refinement with Craig interpolation and symbolic pushdown systems, (TACAS’2006: Tools and Algorithms for the Construction and Analysis of Systems. TACAS’2006: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 3920 (2006), Springer), 489-503 · Zbl 1180.68113 |
| [9] | Goel, A.; Krstic, S.; Tinelli, C., Ground interpolation for combined theories, (Schmidt, R. A., Automated Deduction — CADE-22, 22nd International Conference on Automated Deduction. Proceedings. Automated Deduction — CADE-22, 22nd International Conference on Automated Deduction. Proceedings, LNCS, vol. 5663 (2009)), 183-198 · Zbl 1250.68188 |
| [10] | Henzinger, T. A.; Jhala, R.; Majumdar, R.; McMillan, K. L., Abstractions from proofs, (POPL’2004: Principles of Programming Languages (2004), ACM Press), 232-244 · Zbl 1325.68147 |
| [12] | Jaffar, J.; Michaylov, S., Methodology and implementation of a CLP system, (ICLP’1987: Int. Conf. on Logic Programming, vol. 1 (1987), MIT Press), 196-218 |
| [13] | Jhala, R.; McMillan, K. L., Interpolant-based transition relation approximation, (CAV’2005: Computer Aided Verification. CAV’2005: Computer Aided Verification, Lecture Notes in Computer Science, vol. 3576 (2005), Springer), 39-51 · Zbl 1081.68622 |
| [14] | Jhala, R.; McMillan, K. L., A practical and complete approach to predicate refinement, (TACAS’2006: Tools and Algorithms for the Construction and Analysis of Systems. TACAS’2006: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 3920 (2006), Springer), 459-473 · Zbl 1180.68118 |
| [15] | Kapur, D.; Majumdar, R.; Zarba, C. G., Interpolation for data structures, (FSE’2006: Foundations of Software Engineering (2006), ACM), 105-116 |
| [16] | Koubarakis, M., Tractable disjunctions of linear constraints: basic results and applications to temporal reasoning, Theoretical Computer Science, 266, 1-2, 311-339 (2001) · Zbl 0989.68134 |
| [17] | Kovács, L.; Voronkov, A., Interpolation and symbol elimination, (Schmidt, R. A., Automated Deduction — CADE-22, 22nd International Conference on Automated Deduction. Proceedings. Automated Deduction — CADE-22, 22nd International Conference on Automated Deduction. Proceedings, LNCS, vol. 5663 (2009)), 199-213 · Zbl 1250.68193 |
| [18] | Krajícek, J., Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, Journal of Symbolic Logic, 62, 2, 457-486 (1997) · Zbl 0891.03029 |
| [19] | Lynch, C.; Tang, Y., Interpolants for linear arithmetic in SMT, (Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008. Proceedings. Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008. Proceedings, LNCS, vol. 5311 (2008)), 156-170 · Zbl 1183.68379 |
| [20] | McMillan, K. L., Interpolation and SAT-based model checking, (CAV’2003: Computer Aided Verification. CAV’2003: Computer Aided Verification, LNCS, vol. 2725 (2003), Springer), 1-13 · Zbl 1278.68184 |
| [21] | McMillan, K. L., An interpolating theorem prover, Theoretical Computer Science, 345, 1, 101-121 (2005) · Zbl 1079.68092 |
| [22] | McMillan, K. L., Lazy abstraction with interpolants, (CAV’2006: Computer Aided Verification. CAV’2006: Computer Aided Verification, LNCS, vol. 4144 (2006), Springer), 123-136 · Zbl 1188.68196 |
| [23] | McMillan, K. L., Quantified invariant generation using an interpolating saturation prover, (Ramakrishnan, C. R.; Rehof, J., 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. 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, LNCS, vol. 4963 (2008)), 413-427 · Zbl 1134.68416 |
| [24] | Meyer, R.; Faber, J.; Hoenicke, J.; Rybalchenko, A., Model checking duration calculus: a practical approach, FACS: Formal Aspects of Computing (2008) · Zbl 1151.68487 |
| [25] | Meyer, R.; Faber, J.; Rybalchenko, A., Model checking duration calculus: A practical approach, (ICTAC’2006: Int. Colloq. on Theoretical Aspects of Computing. ICTAC’2006: Int. Colloq. on Theoretical Aspects of Computing, LNCS, vol. 4281 (2006), Springer), 332-346 · Zbl 1168.68425 |
| [26] | Miné, A., The octagon abstract domain, Higher-Order and Symbolic Computation, 19, 1, 31-100 (2006) · Zbl 1105.68069 |
| [27] | Podelski, A.; Rybalchenko, A., ARMC: the logical choice for software model checking with abstraction refinement, (PADL’2007: Practical Aspects of Declarative Languages. PADL’2007: Practical Aspects of Declarative Languages, LNCS, vol. 4354 (2007), Springer), 245-259 |
| [28] | Pudlák, P., Lower bounds for resolution and cutting plane proofs and monotone computations, Journal of Symbolic Logic, 62, 3, 981-998 (1997) · Zbl 0945.03086 |
| [29] | Rybalchenko, A.; Sofronie-Stokkermans, V., Constraint solving for interpolation, (VMCAI (2007)), 346-362 · Zbl 1132.68480 |
| [30] | Schrijver, A., Theory of Linear and Integer Programming (1986), John Wiley & Sons Ltd · Zbl 0665.90063 |
| [31] | Sofronie-Stokkermans, V., Hierarchic reasoning in local theory extensions, (CADE’2005: Int. Conf. on Automated Deduction. CADE’2005: Int. Conf. on Automated Deduction, LNCS, vol. 3632 (2005), Springer), 219-234 · Zbl 1135.03330 |
| [32] | Sofronie-Stokkermans, V., Interpolation in local theory extensions, (IJCAR’2006: Int. Joint Conf. on Automated Reasoning. IJCAR’2006: Int. Joint Conf. on Automated Reasoning, LNCS, vol. 4130 (2006), Springer), 235-250 · Zbl 1222.03018 |
| [33] | Sofronie-Stokkermans, V., Interpolation in local theory extensions, Logical Methods in Computer Science, 4, 4 (2008), Paper 1 · Zbl 1170.03018 |
| [34] | Sontag, E., Real addition and the polynomial hierarchy, Information Processing Letters, 20, 3, 115-120 (1985) · Zbl 0575.03030 |
| [36] | Yorsh, G.; Musuvathi, M., A combination method for generating interpolants, (CADE’2005: Int. Conf. on Automated Deduction. CADE’2005: Int. Conf. on Automated Deduction, LNCS, vol. 3632 (2005), Springer), 353-368 · 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.
