{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:09:13Z","timestamp":1762506553800},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,5,15]],"date-time":"2015-05-15T00:00:00Z","timestamp":1431648000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s00236-015-0236-z","type":"journal-article","created":{"date-parts":[[2015,5,14]],"date-time":"2015-05-14T05:09:33Z","timestamp":1431580173000},"page":"387-424","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Guiding Craig interpolation with domain-specific abstractions"],"prefix":"10.1007","volume":"53","author":[{"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavle","family":"Suboti\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,15]]},"reference":[{"key":"236_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: CAV, pp. 313\u2013329 (2013)","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"236_CR2","doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: LPAR (2012)","DOI":"10.1007\/978-3-642-28717-6_7"},{"issue":"5","key":"236_CR3","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S Bardin","year":"2008","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. 10(5), 401\u2013424 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"236_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: VMCAI. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"236_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV, LNCS, vol. 6806, pp. 184\u2013190. Springer, Berlin (2011). doi: 10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"236_CR6","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) FMCAD, pp. 189\u2013197. IEEE (2010)"},{"key":"236_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: Interpolation for LA+EUF. In: CAV, LNCS, vol. 5123, pp. 304\u2013308. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_29"},{"key":"236_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: CAV, pp. 517\u2013531 (2006)","DOI":"10.1007\/11817963_47"},{"key":"236_CR9","doi-asserted-by":"crossref","unstructured":"Bozga, M., Habermehl, P., Iosif, R., Kone\u010dn\u00fd, F., Vojnar, T.: Automatic verification of integer array programs. In: CAV, pp. 157\u2013172 (2009)","DOI":"10.1007\/978-3-642-02658-4_15"},{"key":"236_CR10","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Proceedings, IJCAR, LNCS. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14203-1_33"},{"key":"236_CR11","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: VMCAI, LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-18275-4_8"},{"key":"236_CR12","doi-asserted-by":"crossref","unstructured":"Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: TACAS, pp. 428\u2013442 (2008)","DOI":"10.1007\/978-3-540-78800-3_32"},{"key":"236_CR13","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Farzan, A., Kincaid, Z.: Consistency analysis of decision-making programs. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 555\u2013568. ACM (2014). doi: 10.1145\/2535838.2535858","DOI":"10.1145\/2535838.2535858"},{"key":"236_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS, LNCS, vol. 8413, pp. 46\u201361. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"236_CR15","doi-asserted-by":"crossref","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Logic 22(3), 250\u2013268 (1957)","DOI":"10.2307\/2963593"},{"key":"236_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"2002","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)","edition":"2"},{"key":"236_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013456. ACM (2013)","DOI":"10.1145\/2509136.2509511"},{"key":"236_CR18","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: VMCAI, pp. 129\u2013145 (2010)","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"236_CR19","first-page":"245","volume":"52","author":"J Esparza","year":"1994","unstructured":"Esparza, J., Nielsen, M.: Decidability issues for Petri nets\u2014a survey. Bull. Eur. Assoc. Theor. Comput. Sci. 52, 245\u2013262 (1994)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"236_CR20","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., Ulbrich, M., R\u00fcmmer, P.: Automating regression verification. In: ASE (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"236_CR21","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: FME, pp. 500\u2013517 (2001)","DOI":"10.1007\/3-540-45251-6_29"},{"key":"236_CR22","unstructured":"Fribourg, L.: Petri nets, flat languages and linear arithmetic. In: Alpuente, M. (ed.) Proceedings of the WFLP\u20192000, pp. 344\u2013365 (2000)"},{"key":"236_CR23","unstructured":"Ganty, P., Majumdar, R.: Algorithmic Verification of Asynchronous Programs. CoRR abs\/1011.0551 (2010)"},{"key":"236_CR24","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, San Francisco (1979)"},{"key":"236_CR25","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"236_CR26","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"236_CR27","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)"},{"key":"236_CR28","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: 31st POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"236_CR29","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"236_CR30","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: SAT, pp. 157\u2013171 (2012)","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"236_CR31","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Playing in the grey area of proofs. In: POPL, pp. 259\u2013272 (2012)","DOI":"10.1145\/2103656.2103689"},{"key":"236_CR32","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Iosif, R., Konecn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: ATVA, pp. 187\u2013202 (2012)","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"236_CR33","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Konecn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems\u2014tool paper. In: FM, pp. 247\u2013251 (2012)","DOI":"10.1007\/978-3-642-32759-9_21"},{"key":"236_CR34","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P., Subotic, P., Yi, W.: Horn clauses for communicating timed systems. In: Workshop on Horn Clauses for Verification and Synthesis (2014)","DOI":"10.4204\/EPTCS.169.6"},{"key":"236_CR35","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(79)90041-0","volume":"8","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135\u2013159 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"236_CR36","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: TACAS, pp. 459\u2013473 (2006)","DOI":"10.1007\/11691372_33"},{"key":"236_CR37","doi-asserted-by":"crossref","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of the STOC\u201982, pp. 267\u2013281. ACM (1982)","DOI":"10.1145\/800070.802201"},{"issue":"1","key":"236_CR38","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0304-3975(92)90173-D","volume":"99","author":"JL Lambert","year":"1992","unstructured":"Lambert, J.L.: A structure to decide reachability in Petri nets. Theor. Comput. Sci. 99(1), 79\u2013104 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"236_CR39","doi-asserted-by":"crossref","unstructured":"Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: Proceedings of the LICS 2009, pp. 4\u201313. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.10"},{"key":"236_CR40","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: Proceedings of the POPL\u201911 (POPL\u201911), pp. 307\u2013316. ACM (2011)","DOI":"10.1145\/1926385.1926421"},{"key":"236_CR41","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: CAV, pp. 592\u2013607 (2013)","DOI":"10.1007\/978-3-642-39799-8_39"},{"key":"236_CR42","doi-asserted-by":"crossref","unstructured":"Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings of the STOC\u201981, pp. 238\u2013246. ACM (1981)","DOI":"10.1145\/800076.802477"},{"key":"236_CR43","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: CAV (2006)","DOI":"10.1007\/11817963_14"},{"key":"236_CR44","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: TACAS, pp. 413\u2013427 (2008)","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"236_CR45","doi-asserted-by":"crossref","unstructured":"Popeea, C., Chin, W.: Dual analysis for proving safety and finding bugs. Sci. Comput. Program. 78(4), 390\u2013411 (2013). doi: 10.1016\/j.scico.2012.07.004","DOI":"10.1016\/j.scico.2012.07.004"},{"key":"236_CR46","doi-asserted-by":"crossref","unstructured":"Rollini, S., Bruttomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: HVC, pp. 182\u2013196 (2010)","DOI":"10.1007\/978-3-642-19583-9_17"},{"key":"236_CR47","doi-asserted-by":"crossref","unstructured":"Rollini, S.F., Alt, L., Fedyukovich, G., Hyv\u00e4rinen, 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\u2013693. Springer, Berlin (2013). doi: 10.1007\/978-3-642-45221-5","DOI":"10.1007\/978-3-642-45221-5"},{"key":"236_CR48","doi-asserted-by":"crossref","unstructured":"Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: CAV, pp. 193\u2013209 (2012)","DOI":"10.1007\/978-3-642-31424-7_18"},{"key":"236_CR49","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Classifying and solving Horn clauses for verification. In: Cohen, E., Rybalchenko, A. (eds.) Verified Software: Theories, Tools, Experiments\u20145th International Conference (VSTTE), LNCS, vol. 8164, pp. 1\u201321. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-54108-7_1"},{"key":"236_CR50","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Computer Aided Verification (CAV), LNCS, vol. 8044, pp. 347\u2013363. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"236_CR51","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Suboti\u0107, P.: Exploring interpolants. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 69\u201376. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679393"},{"key":"236_CR52","doi-asserted-by":"crossref","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Proceedings of the VMCAI, LNCS, vol. 4349, pp. 346\u2013362. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-69738-1_25"},{"key":"236_CR53","doi-asserted-by":"crossref","unstructured":"Seghir, M.N.: A lightweight approach for loop summarization. In: ATVA, pp. 351\u2013365 (2011)","DOI":"10.1007\/978-3-642-24372-1_25"},{"key":"236_CR54","doi-asserted-by":"crossref","unstructured":"Smrcka, A., Vojnar, T.: Verifying parametrised hardware designs via counter automata. In: Haifa Verification Conference, pp. 51\u201368 (2007)","DOI":"10.1007\/978-3-540-77966-7_8"},{"key":"236_CR55","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI, pp. 223\u2013234 (2009)","DOI":"10.1145\/1542476.1542501"},{"key":"236_CR56","doi-asserted-by":"crossref","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: Cavalcanti, A., Dams, D. (eds.) FM, LNCS, vol. 5850, pp. 89\u2013105. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-05089-3_7"},{"key":"236_CR57","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 537\u2013548. ACM (2013)","DOI":"10.1145\/2429069.2429132"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0236-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0236-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0236-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,25]],"date-time":"2019-08-25T02:29:27Z","timestamp":1566700167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0236-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,15]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["236"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0236-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,15]]}}}