{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T03:17:15Z","timestamp":1774063035033,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287169","type":"print"},{"value":"9783642287176","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28717-6_7","type":"book-chapter","created":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T10:13:04Z","timestamp":1331028784000},"page":"46-61","source":"Crossref","is-referenced-by-count":40,"title":["Lazy Abstraction with Interpolants for Arrays"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Alberti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Bruttomesso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy Abstraction with Interpolants for Arrays. extended version, \n                  \n                    http:\/\/homes.dsi.unimi.it\/~ghilardi\/allegati\/ABGRS_LPAR.pdf"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-14203-1_33","volume-title":"Automated Reasoning","author":"A. Brillout","year":"2010","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 384\u2013399. Springer, Heidelberg (2010)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-24288-5_11","volume-title":"Reachability Problems","author":"A. Carioni","year":"2011","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: Automated Termination in Model Checking Modulo Theories. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol.\u00a06945, pp. 110\u2013124. Springer, Heidelberg (2011)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis. In: POPL (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I. Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid Updates: Beyond Strong vs. Weak Updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 246\u2013266. Springer, Heidelberg (2010)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-540-78163-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Dimitrova","year":"2008","unstructured":"Dimitrova, R., Podelski, A.: Is Lazy Abstraction a Decision Procedure for Broadcast Protocols? In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 98\u2013111. Springer, Heidelberg (2008)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191\u2013202 (2002)","DOI":"10.1145\/565816.503291"},{"key":"7_CR9","unstructured":"Ghilardi, S., Ranise, S.: Model Checking Modulo Theory at work: the integration of Yices in MCMT. In: AFM (2009)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. LMCS\u00a06(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14203-1_3","volume-title":"Automated Reasoning","author":"S. Ghilardi","year":"2010","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A Model Checker Modulo Theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 22\u201329. Springer, Heidelberg (2010)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A Framework for Numeric Analysis of Array Operations. In: POPL 2005, pp. 338\u2013350 (2005)","DOI":"10.1145\/1047659.1040333"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Mathias, P.: Discovering Properties about Arrays in Simple Programs. In: PLDI 2008, pp. 339\u2013348 (2008)","DOI":"10.1145\/1375581.1375623"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from Proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array Abstractions from Proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.: Interpolation for Data Structures. In: SIGSOFT 2006\/FSE-14, pp. 105\u2013116 (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 199\u2013213. Springer, Heidelberg (2009)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"7_CR22","unstructured":"Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2006), \n                  \n                    http:\/\/www.SMT-LIB.org"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-03237-0_3","volume-title":"Static Analysis","author":"M.N. Seghir","year":"2009","unstructured":"Seghir, M.N., Podelski, A., Wies, T.: Abstraction Refinement for Quantified Array Assertions. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 3\u201318. Springer, Heidelberg (2009)"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Bryant, R.: Predicate Abstraction with Indexed Predicates. TOCL\u00a09(1) (2007)","DOI":"10.1145\/1297658.1297662"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program Verification using Templates over Predicate Abstraction. In: PLDI (2009)","DOI":"10.1145\/1542476.1542501"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28717-6_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:07:20Z","timestamp":1620112040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28717-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287169","9783642287176"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28717-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}