{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:08:39Z","timestamp":1746194919085},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_16","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T04:25:44Z","timestamp":1418271944000},"page":"282-299","source":"Crossref","is-referenced-by-count":16,"title":["Abstraction of Arrays Based on Non Contiguous Partitions"],"prefix":"10.1007","author":[{"given":"Jiangchao","family":"Liu","sequence":"first","affiliation":[]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol.\u00a08413, pp. 15\u201330. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_2"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)","DOI":"10.1145\/567752.567778"},{"key":"16_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":"16_CR6","doi-asserted-by":"crossref","unstructured":"Cox, A., Chang, B.-Y.E., Rival, X.: Automatic analysis of open objects in dynamic language programs. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 134\u2013150. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-10936-7_9"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-39038-8_17","volume-title":"ECOOP 2013 \u2013 Object-Oriented Programming","author":"A. Cox","year":"2013","unstructured":"Cox, A., Chang, B.-Y.E., Sankaranarayanan, S.: QUIC graphs: Relational invariant generation for containers. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol.\u00a07920, pp. 401\u2013425. Springer, Heidelberg (2013)"},{"key":"16_CR8","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":"16_CR9","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: POPL (2011)","DOI":"10.1145\/1926385.1926407"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-24730-2_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Gopan","year":"2004","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 512\u2013529. Springer, Heidelberg (2004)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL (2005)","DOI":"10.1145\/1040305.1040333"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: PLDI (2008)","DOI":"10.1145\/1375581.1375623"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"16_CR15","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":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"16_CR17","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":"16_CR18","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: HOSC (2006)","DOI":"10.1007\/s10990-006-8609-1"},{"key":"16_CR19","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":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-35182-2_10","volume-title":"Programming Languages and Systems","author":"P. Sotin","year":"2012","unstructured":"Sotin, P., Rival, X.: Hierarchical shape abstraction of dynamic structures in static blocks. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol.\u00a07705, pp. 131\u2013147. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T20:25:41Z","timestamp":1559075141000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}