Guiding Craig interpolation with domain-specific abstractions. (English) Zbl 1344.68139
Summary: Craig interpolation is a standard method to construct and refine abstractions in model checking. To obtain abstractions that are suitable for the verification of software programs or hardware designs, model checkers rely on theorem provers to find the right interpolants, or interpolants containing the right predicates, in a generally infinite lattice of interpolants for any given interpolation problem. We present a semantic and solver-independent framework for systematically exploring interpolant lattices, based on the notion of interpolation abstraction. We discuss how interpolation abstractions can be constructed for a variety of logics, and how they can be applied in the context of software model checking.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03C40 | Interpolation, preservation, definability |
References:
| [1] | Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: CAV, pp. 313-329 (2013) |
| [2] | Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: LPAR (2012) · Zbl 1352.68141 |
| [3] | Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. 10(5), 401-424 (2008) · doi:10.1007/s10009-008-0064-3 |
| [4] | Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: VMCAI. Springer, Berlin (2007) · Zbl 1132.68333 |
| [5] | Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV, LNCS, vol. 6806, pp. 184-190. Springer, Berlin (2011). doi:10.1007/978-3-642-22110-1_16 · Zbl 0769.68104 |
| [6] | Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) FMCAD, pp. 189-197. IEEE (2010) |
| [7] | Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: Interpolation for LA+EUF. In: CAV, LNCS, vol. 5123, pp. 304-308. Springer, Berlin (2008) |
| [8] | Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: CAV, pp. 517-531 (2006) · Zbl 1188.68181 |
| [9] | Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic verification of integer array programs. In: CAV, pp. 157-172 (2009) · Zbl 1242.68063 |
| [10] | Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Proceedings, IJCAR, LNCS. Springer, Berlin (2010) · Zbl 1291.03112 |
| [11] | Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: VMCAI, LNCS. Springer, Berlin (2011) · Zbl 1318.03045 |
| [12] | Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: TACAS, pp. 428-442 (2008) · Zbl 1134.68400 |
| [13] | Chaudhuri, S., Farzan, A., Kincaid, Z.: Consistency analysis of decision-making programs. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 555-568. ACM (2014). doi:10.1145/2535838.2535858 · Zbl 1284.68386 |
| [14] | Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS, LNCS, vol. 8413, pp. 46-61. Springer, Berlin (2014) · Zbl 1368.68245 |
| [15] | Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Logic 22(3), 250-268 (1957) · Zbl 0081.24402 |
| [16] | Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002) · Zbl 1002.06001 · doi:10.1017/CBO9780511809088 |
| [17] | Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Hosking, A.L., Eugster, P.T., Lopes, C.V. (eds.) OOPSLA, pp. 443-456. ACM (2013) · Zbl 1381.68057 |
| [18] | D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: VMCAI, pp. 129-145 (2010) · Zbl 1273.68225 |
| [19] | Esparza, J., Nielsen, M.: Decidability issues for Petri nets—a survey. Bull. Eur. Assoc. Theor. Comput. Sci. 52, 245-262 (1994) · Zbl 0791.68123 |
| [20] | Felsing, D., Grebing, S., Klebanov, V., Ulbrich, M., Rümmer, P.: Automating regression verification. In: ASE (2014) |
| [21] | Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: FME, pp. 500-517 (2001) · Zbl 0977.68671 |
| [22] | Fribourg, L.: Petri nets, flat languages and linear arithmetic. In: Alpuente, M. (ed.) Proceedings of the WFLP’2000, pp. 344-365 (2000) |
| [23] | Ganty, P., Majumdar, R.: Algorithmic Verification of Asynchronous Programs. CoRR abs/1011.0551 (2010) |
| [24] | Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, San Francisco (1979) · Zbl 0411.68039 |
| [25] | Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72-83 (1997) |
| [26] | Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012) |
| [27] | Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009) · Zbl 1178.03001 · doi:10.1017/CBO9780511576430 |
| [28] | Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: 31st POPL (2004) · Zbl 1325.68147 |
| [29] | Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232-244. ACM (2004) · Zbl 1325.68147 |
| [30] | Hoder, K., Bjørner, N.: Generalized property directed reachability. In: SAT, pp. 157-171 (2012) · Zbl 1273.68229 |
| [31] | Hoder, K., Kovács, L., Voronkov, A.: Playing in the grey area of proofs. In: POPL, pp. 259-272 (2012) · Zbl 1321.68196 |
| [32] | Hojjat, H., Iosif, R., Konecný, F., Kuncak, V., Rümmer, P.: Accelerating interpolants. In: ATVA, pp. 187-202 (2012) · Zbl 1374.68291 |
| [33] | Hojjat, H., Konecný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems—tool paper. In: FM, pp. 247-251 (2012) |
| [34] | Hojjat, H., Rümmer, P., Subotic, P., Yi, W.: Horn clauses for communicating timed systems. In: Workshop on Horn Clauses for Verification and Synthesis (2014) · Zbl 1464.68207 |
| [35] | Hopcroft, J.E., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135-159 (1979) · Zbl 0466.68048 · doi:10.1016/0304-3975(79)90041-0 |
| [36] | Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: TACAS, pp. 459-473 (2006) · Zbl 1180.68118 |
| [37] | Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of the STOC’82, pp. 267-281. ACM (1982) |
| [38] | Lambert, J.L.: A structure to decide reachability in Petri nets. Theor. Comput. Sci. 99(1), 79-104 (1992) · Zbl 0769.68104 · doi:10.1016/0304-3975(92)90173-D |
| [39] | Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: Proceedings of the LICS 2009, pp. 4-13. IEEE Computer Society (2009) |
| [40] | Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: Proceedings of the POPL’11 (POPL’11), pp. 307-316. ACM (2011) · Zbl 1284.68429 |
| [41] | Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: CAV, pp. 592-607 (2013) |
| [42] | Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings of the STOC’81, pp. 238-246. ACM (1981) |
| [43] | McMillan, K.L.: Lazy abstraction with interpolants. In: CAV (2006) · Zbl 1188.68196 |
| [44] | McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: TACAS, pp. 413-427 (2008) · Zbl 1134.68416 |
| [45] | Popeea, C., Chin, W.: Dual analysis for proving safety and finding bugs. Sci. Comput. Program. 78(4), 390-411 (2013). doi:10.1016/j.scico.2012.07.004 · Zbl 1264.68065 |
| [46] | Rollini, S., Bruttomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: HVC, pp. 182-196 (2010) · Zbl 1325.68215 |
| [47] | Rollini, S.F., Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: Periplo: A framework for producing effective interpolants in sat-based software verification. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) LPAR, LNCS, vol. 8312, pp. 683-693. Springer, Berlin (2013). doi:10.1007/978-3-642-45221-5 · Zbl 1407.68303 |
| [48] | Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: CAV, pp. 193-209 (2012) |
| [49] | Rümmer, P., Hojjat, H., Kuncak, V.: Classifying and solving Horn clauses for verification. In: Cohen, E., Rybalchenko, A. (eds.) Verified Software: Theories, Tools, Experiments—5th International Conference (VSTTE), LNCS, vol. 8164, pp. 1-21. Springer, Berlin (2013) · Zbl 1322.68134 |
| [50] | Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Computer Aided Verification (CAV), LNCS, vol. 8044, pp. 347-363. Springer, Berlin (2013) |
| [51] | Rümmer, P., Subotić, P.: Exploring interpolants. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 69-76. IEEE (2013) |
| [52] | Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Proceedings of the VMCAI, LNCS, vol. 4349, pp. 346-362. Springer, Berlin (2007) · Zbl 1132.68480 |
| [53] | Seghir, M.N.: A lightweight approach for loop summarization. In: ATVA, pp. 351-365 (2011) · Zbl 1348.68150 |
| [54] | Smrcka, A., Vojnar, T.: Verifying parametrised hardware designs via counter automata. In: Haifa Verification Conference, pp. 51-68 (2007) |
| [55] | Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI, pp. 223-234 (2009) · Zbl 0791.68123 |
| [56] | Tonetta, S.: Abstract model checking without computing the abstraction. In: Cavalcanti, A., Dams, D. (eds.) FM, LNCS, vol. 5850, pp. 89-105. Springer, Berlin (2009) |
| [57] | Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 537-548. ACM (2013) · Zbl 1301.68106 |
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.
