{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T04:43:31Z","timestamp":1789879411497,"version":"4.0.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,4,15]],"date-time":"2016-04-15T00:00:00Z","timestamp":1460678400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,4,15]],"date-time":"2016-04-15T00:00:00Z","timestamp":1460678400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["CCF-1320583"],"award-info":[{"award-number":["CCF-1320583"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s10817-016-9371-7","type":"journal-article","created":{"date-parts":[[2016,4,15]],"date-time":"2016-04-15T08:01:18Z","timestamp":1460707278000},"page":"37-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Complete Instantiation-Based Interpolation"],"prefix":"10.1007","volume":"57","author":[{"given":"Nishant","family":"Totla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,4,15]]},"reference":[{"key":"9371_CR1","doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: LPAR, LNCS, vol. 7180. Springer, pp. 46\u201361 (2012)","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"9371_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF02485230","volume":"5","author":"P Bacsich","year":"1975","unstructured":"Bacsich, P.: Amalgamation properties and interpolation theorems for equational theories. Algebra Univ. 5, 45\u201355 (1975)","journal-title":"Algebra Univ."},{"key":"9371_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: To goto where no statement has gone before. In: VSTTE, LNCS, vol. 6217, pp. 157\u2013168 (2010)","DOI":"10.1007\/978-3-642-15057-9_11"},{"key":"9371_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: CAV, LNCS, vol. 4144. Springer, pp. 532\u2013546 (2006)","DOI":"10.1007\/11817963_48"},{"key":"9371_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: Interpolation for LA+EUF. In: CAV, LNCS, vol. 5123, pp. 304\u2013308 (2008)","DOI":"10.1007\/978-3-540-70545-1_29"},{"issue":"4","key":"9371_CR6","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10817-011-9237-y","volume":"47","author":"A Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. J. Autom. Reason. 47(4), 341\u2013367 (2011)","journal-title":"J. Autom. Reason."},{"key":"9371_CR7","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, vol. 6538. Springer, pp. 88\u2013102 (2011)","DOI":"10.1007\/978-3-642-18275-4_8"},{"key":"9371_CR8","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Rewriting-based quantifier-free interpolation for a theory of arrays. In: RTA, LIPIcs, vol. 10, pp. 171\u2013186 (2011)"},{"key":"9371_CR9","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: From strong amalgamability to modularity of quantifier-free interpolation. In: IJCAR, LNCS, vol. 7364. Springer, pp. 118\u2013133 (2012)","DOI":"10.1007\/978-3-642-31365-3_12"},{"key":"9371_CR10","doi-asserted-by":"crossref","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: TACAS, LNCS, vol. 7795. Springer, pp. 124\u2013138 (2013)","DOI":"10.1007\/978-3-642-36742-7_9"},{"issue":"3","key":"9371_CR11","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand\u2013Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269\u2013285 (1957)","journal-title":"J. Symb. Log."},{"key":"9371_CR12","doi-asserted-by":"crossref","unstructured":"Dr\u00e4ger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: a certifying model checker for infinite-state concurrent systems. In: TACAS, LNCS, vol. 6015. Springer, pp. 271\u2013274 (2010)","DOI":"10.1007\/978-3-642-12002-2_22"},{"key":"9371_CR13","doi-asserted-by":"crossref","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: FM, LNCS, vol. 7436. Springer, pp. 187\u2013201 (2012)","DOI":"10.1007\/978-3-642-32759-9_17"},{"key":"9371_CR14","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: CAV, LNCS, vol. 4590. Springer, pp. 173\u2013177 (2007)","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"9371_CR15","doi-asserted-by":"crossref","unstructured":"Fuchs, A., Goel, A., Grundy, J., Krstic, S., Tinelli, C.: Ground interpolation for the theory of equality. In: TACAS, LNCS, vol. 5505. Springer, pp. 413\u2013427 (2009)","DOI":"10.1007\/978-3-642-00768-2_34"},{"key":"9371_CR16","doi-asserted-by":"crossref","unstructured":"Goel, A., Krstic, S., Tinelli, C.: Ground interpolation for combined theories. In: CADE, Lecture Notes in Computer Science, vol. 5663. Springer, pp. 183\u2013198 (2009)","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"9371_CR17","doi-asserted-by":"crossref","unstructured":"Griggio, A., Le, T.T.H., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In: TACAS, LNCS, vol. 6605. Springer, pp. 143\u2013157 (2011)","DOI":"10.1007\/978-3-642-19835-9_13"},{"key":"9371_CR18","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL. ACM, pp. 471\u2013482 (2010)","DOI":"10.1145\/1707801.1706353"},{"key":"9371_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.L: Abstractions from proofs. In: 31st POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"9371_CR20","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination in vampire. In: IJCAR, LNCS, vol. 6173. Springer, pp. 188\u2013195 (2010)","DOI":"10.1007\/978-3-642-14203-1_16"},{"key":"9371_CR21","doi-asserted-by":"crossref","unstructured":"Ihlemann, C.: Reasoning in Combinations of Theories. PhD thesis, Saarland University (2010)","DOI":"10.1007\/978-3-642-14203-1_4"},{"key":"9371_CR22","doi-asserted-by":"crossref","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: TACAS, pp. 265\u2013281 (2008)","DOI":"10.1007\/978-3-540-78800-3_19"},{"key":"9371_CR23","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. Log. Methods Comput. Sci. 3(4), 1\u201317 (2007)"},{"key":"9371_CR24","doi-asserted-by":"crossref","first-page":"193","DOI":"10.7146\/math.scand.a-10468","volume":"4","author":"B J\u00f3nsson","year":"1956","unstructured":"J\u00f3nsson, B.: Universal relational systems. Math. Scand. 4, 193\u2013208 (1956)","journal-title":"Math. Scand."},{"key":"9371_CR25","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT FSE. ACM, pp. 105\u2013116 (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"9371_CR26","doi-asserted-by":"crossref","unstructured":"Kroening, D., Weissenbacher, G.: Interpolation-based software verification with wolverine. In: CAV, LNCS, vol. 6806. Springer, pp. 573\u2013578 (2011)","DOI":"10.1007\/978-3-642-22110-1_45"},{"key":"9371_CR27","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: POPL. ACM, pp. 171\u2013182 (2008)","DOI":"10.1145\/1328897.1328461"},{"key":"9371_CR28","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21\u201328 (1962)"},{"key":"9371_CR29","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV, LNCS, vol. 2725. Springer, pp. 1\u201313 (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"issue":"1","key":"9371_CR30","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9371_CR31","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: CAV, LNCS, vol. 4144. Springer, pp. 123\u2013136 (2006)","DOI":"10.1007\/11817963_14"},{"key":"9371_CR32","doi-asserted-by":"crossref","unstructured":"McMillan, KL.: Quantified invariant generation using an interpolating saturation prover. In: TACAS, LNCS, vol. 4963. Springer, pp. 413\u2013427 (2008)","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"9371_CR33","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: POPL. ACM, pp. 38\u201347 (1983)","DOI":"10.1145\/567067.567073"},{"key":"9371_CR34","doi-asserted-by":"crossref","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: POPL. ACM, pp. 249\u2013260 (2010)","DOI":"10.1145\/1707801.1706330"},{"key":"9371_CR35","doi-asserted-by":"crossref","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: VMCAI, LNCS, vol. 4349. Springer, pp. 346\u2013362 (2007)","DOI":"10.1007\/978-3-540-69738-1_25"},{"issue":"3","key":"9371_CR36","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"9371_CR37","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: CADE, pp. 219\u2013234 (2005)","DOI":"10.1007\/11532231_16"},{"key":"9371_CR38","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Log. Methods Comput. Sci. 4(4), 1\u201331 (2008)"},{"key":"9371_CR39","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. CoRR, abs\/0806.4553 (2008)","DOI":"10.2168\/LMCS-4(4:1)2008"},{"key":"9371_CR40","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: POPL. ACM (2013, to appear)","DOI":"10.1145\/2429069.2429132"},{"key":"9371_CR41","doi-asserted-by":"crossref","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: CADE, LNCS, vol. 6803. Springer, pp. 476\u2013491 (2011)","DOI":"10.1007\/978-3-642-22438-6_36"},{"key":"9371_CR42","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: CADE, LNCS, vol. 3632, pp. 353\u2013368 (2005)","DOI":"10.1007\/11532231_26"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9371-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9371-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9371-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9371-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T22:59:27Z","timestamp":1589410767000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9371-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,15]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["9371"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9371-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,15]]},"assertion":[{"value":"29 March 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 April 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 April 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}