{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:29Z","timestamp":1772164049355,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T00:00:00Z","timestamp":1358899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,1,23]]},"DOI":"10.1145\/2429069.2429132","type":"proceedings-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T10:29:29Z","timestamp":1358850569000},"page":"537-548","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Complete instantiation-based interpolation"],"prefix":"10.1145","author":[{"given":"Nishant","family":"Totla","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Bombay, Bombay, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"New York University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,1,23]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02485230"},{"key":"e_1_3_2_2_3_1","series-title":"LNCS","first-page":"157","volume-title":"VSTTE","author":"Barnett M.","year":"2010","unstructured":"M. Barnett and K. R. M. Leino . To goto where no statement has gone before . In VSTTE , volume 6217 of LNCS , pages 157 -- 168 , 2010 . M. Barnett and K. R. M. Leino. To goto where no statement has gone before. In VSTTE, volume 6217 of LNCS, pages 157--168, 2010."},{"key":"e_1_3_2_2_4_1","volume-title":"The SMT-LIB Standard: Version 2.0","author":"Barrett C.","year":"2010","unstructured":"C. Barrett , A. Stump , and C. Tinelli . The SMT-LIB Standard: Version 2.0 , 2010 . C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0, 2010."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_48"},{"key":"e_1_3_2_2_6_1","unstructured":"D. Beyer D. Zufferey and R. Majumdar. CSIsat: Interpolation for LA  D. Beyer D. Zufferey and R. Majumdar. CSIsat: Interpolation for LA"},{"key":"e_1_3_2_2_7_1","unstructured":"EUF.\n     In CAV volume \n  5123\n   of \n  LNCS pages \n  304\n  --\n  308 2008\n  .  EUF. In CAV volume 5123 of LNCS pages 304--308 2008."},{"key":"e_1_3_2_2_8_1","series-title":"LNCS","first-page":"102","volume-title":"MPC","author":"Bornat R.","year":"2000","unstructured":"R. Bornat . Proving Pointer Programs in Hoare Logic . In MPC , volume 1837 of LNCS , pages 102 -- 126 . Springer , 2000 . R. Bornat. Proving Pointer Programs in Hoare Logic. In MPC, volume 1837 of LNCS, pages 102--126. Springer, 2000."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9237-y"},{"key":"e_1_3_2_2_10_1","series-title":"LNCS","first-page":"88","volume-title":"VMCAI","author":"Brillout A.","year":"2011","unstructured":"A. Brillout , D. Kroening , P. R\u00fcmmer , and T. Wahl . Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic . In VMCAI , volume 6538 of LNCS , pages 88 -- 102 . Springer , 2011 . A. Brillout, D. Kroening, P. R\u00fcmmer, and T. Wahl. Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. In VMCAI, volume 6538 of LNCS, pages 88--102. Springer, 2011."},{"key":"e_1_3_2_2_11_1","series-title":"LIPIcs","first-page":"171","volume-title":"RTA","author":"Bruttomesso R.","year":"2011","unstructured":"R. Bruttomesso , S. Ghilardi , and S. Ranise . Rewriting-based quantifier-free interpolation for a theory of arrays . In RTA , volume 10 of LIPIcs , pages 171 -- 186 , 2011 . R. Bruttomesso, S. Ghilardi, and S. Ranise. Rewriting-based quantifier-free interpolation for a theory of arrays. In RTA, volume 10 of LIPIcs, pages 171--186, 2011."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_12"},{"key":"e_1_3_2_2_13_1","series-title":"LNCS","first-page":"456","volume-title":"FOSSACS","author":"Cousot P.","year":"2011","unstructured":"P. Cousot , R. Cousot , and L. Mauborgne . The reduced product of abstract domains and the combination of decision procedures . In FOSSACS , volume 6604 of LNCS , pages 456 -- 472 . Springer , 2011 . P. Cousot, R. Cousot, and L. Mauborgne. The reduced product of abstract domains and the combination of decision procedures. In FOSSACS, volume 6604 of LNCS, pages 456--472. Springer, 2011."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_22"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"e_1_3_2_2_18_1","series-title":"LNCS","first-page":"187","volume-title":"FM","author":"Ermis E.","year":"2012","unstructured":"E. Ermis , M. Sch\\\"af, and T. Wies . Error invariants . In FM , volume 7436 of LNCS , pages 187 -- 201 . Springer , 2012 . E. Ermis, M. Sch\\\"af, and T. Wies. Error invariants. In FM, volume 7436 of LNCS, pages 187--201. Springer, 2012."},{"key":"e_1_3_2_2_19_1","series-title":"LNCS","first-page":"173","volume-title":"CAV","author":"Filli\u00e2tre J.-C.","year":"2007","unstructured":"J.-C. Filli\u00e2tre and C. March\u00e9 . The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification . In CAV , volume 4590 of LNCS , pages 173 -- 177 . Springer , 2007 . J.-C. Filli\u00e2tre and C. March\u00e9. The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In CAV, volume 4590 of LNCS, pages 173--177. Springer, 2007."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_34"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"e_1_3_2_2_23_1","first-page":"1","volume":"8","author":"Griggio A.","year":"2012","unstructured":"A. Griggio . A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT , 8 : 1 -- 27 , January 2012 . A. Griggio. A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT, 8:1--27, January 2012.","journal-title":"Satisfiability Modulo Linear Integer Arithmetic. JSAT"},{"key":"e_1_3_2_2_24_1","series-title":"LNCS","first-page":"143","volume-title":"TACAS","author":"Griggio A.","year":"2011","unstructured":"A. Griggio , T. T. H. Le , and R. Sebastiani . Efficient interpolant generation in satisfiability modulo linear integer arithmetic . In TACAS , volume 6605 of LNCS , pages 143 -- 157 . Springer , 2011 . A. Griggio, T. T. H. Le, and R. Sebastiani. Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In TACAS, volume 6605 of LNCS, pages 143--157. Springer, 2011."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706353"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_16"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103689"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792759"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_29"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_3_2_2_32_1","volume-title":"Interpolant-based transition relation approximation. Logical Methods in Computer Science, 3(4)","author":"Jhala R.","year":"2007","unstructured":"R. Jhala and K. L. McMillan . Interpolant-based transition relation approximation. Logical Methods in Computer Science, 3(4) , 2007 . R. Jhala and K. L. McMillan. Interpolant-based transition relation approximation. Logical Methods in Computer Science, 3(4), 2007."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.7146\/math.scand.a-10468"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181789"},{"key":"e_1_3_2_2_35_1","series-title":"LNCS","first-page":"573","volume-title":"CAV","author":"Kroening D.","year":"2011","unstructured":"D. Kroening and G. Weissenbacher . Interpolation-Based Software Verification with Wolverine . In CAV , volume 6806 of LNCS , pages 573 -- 578 . Springer , 2011 . D. Kroening and G. Weissenbacher. Interpolation-Based Software Verification with Wolverine. In CAV, volume 6806 of LNCS, pages 573--578. Springer, 2011."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_3_2_2_37_1","first-page":"21","volume-title":"IFIP Congress","author":"McCarthy J.","year":"1962","unstructured":"J. McCarthy . Towards a mathematical science of computation . In IFIP Congress , pages 21 -- 28 , 1962 . J. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962."},{"key":"e_1_3_2_2_38_1","series-title":"LNCS","first-page":"1","volume-title":"CAV","author":"McMillan K. L.","year":"2003","unstructured":"K. L. McMillan . Interpolation and SAT-Based Model Checking . In CAV , volume 2725 of LNCS , pages 1 -- 13 . Springer , 2003 . K. L. McMillan. Interpolation and SAT-Based Model Checking. In CAV, volume 2725 of LNCS, pages 1--13. Springer, 2003."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_2_41_1","series-title":"LNCS","first-page":"413","volume-title":"TACAS","author":"McMillan K. L.","year":"2008","unstructured":"K. L. McMillan . Quantified invariant generation using an interpolating saturation prover . In TACAS , volume 4963 of LNCS , pages 413 -- 427 . Springer , 2008 . K. L. McMillan. Quantified invariant generation using an interpolating saturation prover. In TACAS, volume 4963 of LNCS, pages 413--427. Springer, 2008."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567073"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706330"},{"key":"e_1_3_2_2_44_1","series-title":"LNCS","first-page":"252","volume-title":"VMCAI","author":"Reps T. W.","year":"2004","unstructured":"T. W. Reps , S. Sagiv , and G. Yorsh . Symbolic implementation of the best transformer . In VMCAI , volume 2937 of LNCS , pages 252 -- 266 . Springer , 2004 . T. W. Reps, S. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. In VMCAI, volume 2937 of LNCS, pages 252--266. Springer, 2004."},{"key":"e_1_3_2_2_45_1","series-title":"LNCS","first-page":"346","volume-title":"VMCAI","author":"Rybalchenko A.","year":"2007","unstructured":"A. Rybalchenko and V. Sofronie-Stokkermans . Constraint solving for interpolation . In VMCAI , volume 4349 of LNCS , pages 346 -- 362 . Springer , 2007 . A. Rybalchenko and V. Sofronie-Stokkermans. Constraint solving for interpolation. In VMCAI, volume 4349 of LNCS, pages 346--362. Springer, 2007."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_16"},{"key":"e_1_3_2_2_48_1","volume-title":"Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4)","author":"Sofronie-Stokkermans V.","year":"2008","unstructured":"V. Sofronie-Stokkermans . Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4) , 2008 . V. Sofronie-Stokkermans. Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4), 2008."},{"key":"e_1_3_2_2_50_1","series-title":"LNCS","first-page":"476","volume-title":"CADE","author":"Wies T.","year":"2011","unstructured":"T. Wies , M. Mu\\ niz, and V. Kuncak . An efficient decision procedure for imperative tree data structures . In CADE , volume 6803 of LNCS , pages 476 -- 491 . Springer , 2011 . T. Wies, M. Mu\\ niz, and V. Kuncak. An efficient decision procedure for imperative tree data structures. In CADE, volume 6803 of LNCS, pages 476--491. Springer, 2011."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_26"}],"event":{"name":"POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Rome Italy","acronym":"POPL '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429132","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2429069.2429132","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:35Z","timestamp":1750221335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429132"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,23]]},"references-count":50,"alternative-id":["10.1145\/2429069.2429132","10.1145\/2429069"],"URL":"https:\/\/doi.org\/10.1145\/2429069.2429132","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2480359.2429132","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,1,23]]},"assertion":[{"value":"2013-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}