Interpolant generation for UTVPI. (English) Zbl 1250.68186
Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 167-182 (2009).
Summary: The problem of computing Craig interpolants in SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for interpolant generation have been presented for some theories of interest – including that of equality and uninterpreted functions (\(\mathcal{EUF}\)), linear arithmetic over the rationals \((\mathcal{LA}(\mathbb{Q}))\), and some fragments of linear arithmetic over the integers \((\mathcal{LA}(\mathbb{Z}))\) – and they are successfully used within model checking tools.
In this paper we address the problem of computing interpolants in the theory of Unit-Two-Variable-Per-Inequality (\(\mathcal{UTVPI}\)). This theory is a very useful fragment of \(\mathcal{LA}(\mathbb{Z})\), since it is expressive enough to encode many hardware and software verification queries while still admitting a polynomial time decision procedure. We present an efficient graph-based algorithm for interpolant generation in \(\mathcal{UTVPI}\), which exploits the power of modern SMT techniques. We have implemented our new algorithm within the MathSAT SMT solver. Our experimental evaluation demonstrates both the efficiency and the usefulness of the new algorithm.
For the entire collection see [Zbl 1167.68006].
In this paper we address the problem of computing interpolants in the theory of Unit-Two-Variable-Per-Inequality (\(\mathcal{UTVPI}\)). This theory is a very useful fragment of \(\mathcal{LA}(\mathbb{Z})\), since it is expressive enough to encode many hardware and software verification queries while still admitting a polynomial time decision procedure. We present an efficient graph-based algorithm for interpolant generation in \(\mathcal{UTVPI}\), which exploits the power of modern SMT techniques. We have implemented our new algorithm within the MathSAT SMT solver. Our experimental evaluation demonstrates both the efficiency and the usefulness of the new algorithm.
For the entire collection see [Zbl 1167.68006].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
| 03C40 | Interpolation, preservation, definability |
References:
| [1] | Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 457–461. Springer, Heidelberg (2004) · Zbl 1103.68604 · doi:10.1007/978-3-540-27813-9_36 |
| [2] | Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast: Applications to software engineering. STTT 9(5-6), 505–525 (2007) · doi:10.1007/s10009-007-0044-z |
| [3] | Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: Interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 304–308. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-70545-1_29 |
| [4] | Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-70545-1_28 |
| [5] | Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008) · Zbl 1134.68402 · doi:10.1007/978-3-540-78800-3_30 |
| [6] | Cotton, S., Maler, O.: Fast and Flexible Difference Constraint Propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006) · Zbl 1187.68537 · doi:10.1007/11814948_19 |
| [7] | Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: PLDI (2002) · doi:10.1145/512529.512558 |
| [8] | Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL. ACM, New York (2004) · Zbl 1325.68147 |
| [9] | Jaffar, J., Maher, M.J., Stuckey, P.J., Yap, R.H.C.: Beyond Finite Domains. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874. Springer, Heidelberg (1994) · doi:10.1007/3-540-58601-6_92 |
| [10] | Jain, H., Clarke, E.M., Grumberg, O.: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 254–267. Springer, Heidelberg (2008) · Zbl 1155.68439 · doi:10.1007/978-3-540-70545-1_24 |
| [11] | Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006) · Zbl 1180.68118 · doi:10.1007/11691372_33 |
| [12] | Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Young, M., Devanbu, P.T. (eds.) SIGSOFT FSE. ACM, New York (2006) |
| [13] | Kroening, D., Weissenbacher, G.: Lifting Propositional Interpolants to the Word-Level. In: FMCAD, pp. 85–89. IEEE Computer Society, Los Alamitos (2007) |
| [14] | Krstić, S., Fuchs, A., Goel, A., Grundy, J., Tinelli, C.: Ground Interpolation for the Theory of Equality. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 413–427. Springer, Heidelberg (2009) · Zbl 1234.68257 |
| [15] | Lahiri, S.K., Bryant, R.E.: Deductive Verification of Advanced Out-of-Order Microprocessors. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 341–354. Springer, Heidelberg (2003) · Zbl 1278.68180 · doi:10.1007/978-3-540-45069-6_33 |
| [16] | Lahiri, S.K., Musuvathi, M.: An Efficient Decision Procedure for UTVPI Constraints. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol. 3717, pp. 168–183. Springer, Heidelberg (2005) · Zbl 1171.68715 · doi:10.1007/11559306_9 |
| [17] | McMillan, K.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) · Zbl 1278.68184 · doi:10.1007/978-3-540-45069-6_1 |
| [18] | McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1) (2005) · Zbl 1079.68092 · doi:10.1016/j.tcs.2005.07.003 |
| [19] | McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006) · Zbl 1188.68196 · doi:10.1007/11817963_14 |
| [20] | Miné, A.: The Octagon Abstract Domain. In: Proc. of WCRE, Washington, DC, USA, pp. 310–319. IEEE Computer Society, Los Alamitos (2001) |
| [21] | Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005) · Zbl 1081.68629 · doi:10.1007/11513988_33 |
| [22] | Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007) · Zbl 1132.68480 · doi:10.1007/978-3-540-69738-1_25 |
| [23] | Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT 3 (2007) · Zbl 1145.68501 |
| [24] | Seshia, S.A., Bryant, R.E.: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. In: LICS. IEEE Computer Society, Los Alamitos (2004) · Zbl 1125.03010 |
| [25] | Sofronie-Stokkermans, V.: Interpolation in Local Theory Extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 235–250. Springer, Heidelberg (2006) · Zbl 1222.03018 · doi:10.1007/11814771_21 |
| [26] | Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 353–368. Springer, Heidelberg (2005) · Zbl 1135.03331 · doi:10.1007/11532231_26 |
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.
