{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:26:37Z","timestamp":1746001597620},"reference-count":33,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Computer Languages, Systems & Structures"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1016\/j.cl.2016.01.005","type":"journal-article","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T12:34:22Z","timestamp":1453984462000},"page":"104-129","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"special_numbering":"P1","title":["An array content static analysis based on non-contiguous partitions"],"prefix":"10.1016","volume":"47","author":[{"given":"Jiangchao","family":"Liu","sequence":"first","affiliation":[]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.cl.2016.01.005_bib1","doi-asserted-by":"crossref","unstructured":"Alberti Francesco, Ghilardi Silvio, Sharygina Natasha. Definability of accelerated relations in a theory of arrays and its applications. In: Symposium on frontiers of combining systems (FCS); 2013. p. 23\u201339.","DOI":"10.1007\/978-3-642-40885-4_3"},{"key":"10.1016\/j.cl.2016.01.005_bib2","doi-asserted-by":"crossref","unstructured":"Alberti Francesco, Ghilardi Silvio, Sharygina Natasha. Decision procedures for flat array properties. In: Tools and algorithms for the construction and analysis of systems (TACAS); 2014. p. 15\u201330.","DOI":"10.1007\/978-3-642-54862-8_2"},{"key":"10.1016\/j.cl.2016.01.005_bib3","doi-asserted-by":"crossref","unstructured":"Beyer Dirk, Henzinger Thomas A, Majumdar Rupak, Rybalchenko Andrey. Invariant synthesis for combined theories. In: Verification, model checking, and abstract interpretation (VMCAI); 2007. p. 378\u201394.","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"10.1016\/j.cl.2016.01.005_bib4","doi-asserted-by":"crossref","unstructured":"Blanchet Bruno, Cousot Patrick, Cousot Radhia, Feret J\u00e9r\u00f4me, Mauborgne Laurent, Min\u00e9 Antoine, et al. A static analyzer for large safety-critical software. In: ACM SIGPLAN conference on programming language design and implementation (PLDI); 2003. p. 196\u2013207.","DOI":"10.1145\/780822.781153"},{"key":"10.1016\/j.cl.2016.01.005_bib5","doi-asserted-by":"crossref","unstructured":"Bradley Aaron R, Manna Zohar, Sipma Henny B. What\u05f3s decidable about arrays? In: Verification, model checking, and abstract interpretation (VMCAI); 2006. p. 427\u201342.","DOI":"10.1007\/11609773_28"},{"key":"10.1016\/j.cl.2016.01.005_bib6","doi-asserted-by":"crossref","unstructured":"Evan Chang Bor-Yuh, Rival Xavier. Relational inductive shape analysis. In: ACM symposium on principles of programming languages (POPL); 2008. p. 247\u201360.","DOI":"10.1145\/1328897.1328469"},{"key":"10.1016\/j.cl.2016.01.005_bib7","doi-asserted-by":"crossref","unstructured":"Evan Chang Bor-Yuh, Rival Xavier. Modular construction of shape-numeric analyzers. In: Semantics, abstract interpretation, and reasoning about programs (SAIRP); 2013. p. 161\u201385.","DOI":"10.4204\/EPTCS.129.11"},{"key":"10.1016\/j.cl.2016.01.005_bib8","doi-asserted-by":"crossref","unstructured":"Evan Chang Bor-Yuh, Rival Xavier, Necula George C. Shape analysis with structural invariant checkers. In: Static analysis symposium (SAS); 2007. p. 384\u2013401.","DOI":"10.1007\/978-3-540-74061-2_24"},{"key":"10.1016\/j.cl.2016.01.005_bib9","doi-asserted-by":"crossref","unstructured":"Chen Liqian, Min\u00e9 Antoine, Cousot Patrick. A sound floating-point polyhedra abstract domain. In: Asian symposium on programming languages and systems (APLAS); 2008. p. 3\u201318.","DOI":"10.1007\/978-3-540-89330-1_2"},{"key":"10.1016\/j.cl.2016.01.005_bib10","doi-asserted-by":"crossref","unstructured":"Cousot Patrick, Cousot Radhia. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM symposium on principles of programming languages (POPL); 1977. p. 238\u201352.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/j.cl.2016.01.005_bib11","doi-asserted-by":"crossref","unstructured":"Cousot Patrick, Cousot Radhia. Systematic design of program analysis frameworks. In: ACM symposium on principles of programming languages (POPL); 1979. p. 269\u201382.","DOI":"10.1145\/567752.567778"},{"key":"10.1016\/j.cl.2016.01.005_bib12","doi-asserted-by":"crossref","unstructured":"Cousot Patrick, Cousot Radhia, Logozzo Francesco. A parametric segmentation functor for fully automatic and scalable array content analysis. In: ACM symposium on principles of programming languages (POPL); 2011. p. 105\u201318.","DOI":"10.1145\/1925844.1926399"},{"key":"10.1016\/j.cl.2016.01.005_bib13","doi-asserted-by":"crossref","unstructured":"Cox Arlen, Evan Chang Bor-Yuh, Rival Xavier. Automatic analysis of open objects in dynamic language programs. In: Static analysis symposium (SAS); 2014. p. 134\u201350.","DOI":"10.1007\/978-3-319-10936-7_9"},{"key":"10.1016\/j.cl.2016.01.005_bib14","doi-asserted-by":"crossref","unstructured":"Cox Arlen, Evan Chang Bor-Yuh, Sankaranarayanan Sriram. QUIC graphs: relational invariant generation for containers. In: European conference on object-oriented programming (ECOOP); 2013. p. 401\u201325.","DOI":"10.1007\/978-3-642-39038-8_17"},{"key":"10.1016\/j.cl.2016.01.005_bib15","doi-asserted-by":"crossref","unstructured":"Dillig Isil, Dillig Thomas, Aiken Alex. Fluid updates: beyond strong vs. weak updates. In: European symposium on programming (ESOP); 2010. p. 246\u201366.","DOI":"10.1007\/978-3-642-11957-6_14"},{"key":"10.1016\/j.cl.2016.01.005_bib16","doi-asserted-by":"crossref","unstructured":"Dillig Isil, Dillig Thomas, Aiken Alex. Precise reasoning for programs using containers. In: ACM symposium on principles of programming languages (POPL); 2011. p. 187\u2013200.","DOI":"10.1145\/1925844.1926407"},{"key":"10.1016\/j.cl.2016.01.005_bib17","doi-asserted-by":"crossref","unstructured":"Gopan Denis, DiMaio Frank, Dor Nurit, Reps Thomas W, Sagiv Shmuel. Numeric domains with summarized dimensions. In: Tools and algorithms for the construction and analysis of systems (TACAS); 2004. p. 512\u201329.","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"10.1016\/j.cl.2016.01.005_bib18","doi-asserted-by":"crossref","unstructured":"Gopan Denis, Reps Thomas W, Sagiv Shmuel. A framework for numeric analysis of array operations. In: ACM symposium on principles of programming languages (POPL); 2005. p. 338\u201350.","DOI":"10.1145\/1047659.1040333"},{"key":"10.1016\/j.cl.2016.01.005_bib19","doi-asserted-by":"crossref","unstructured":"Gulwani Sumit, McCloskey Bill, Tiwari Ashish. Lifting abstract interpreters to quantified logical domains. In: ACM symposium on principles of programming languages (POPL); 2008. p. 235\u201346.","DOI":"10.1145\/1328897.1328468"},{"key":"10.1016\/j.cl.2016.01.005_bib20","doi-asserted-by":"crossref","unstructured":"Halbwachs Nicolas, P\u00e9ron Mathias. Discovering properties about arrays in simple programs. In: ACM SIGPLAN conference on programming language design and implementation (PLDI); 2008. p. 339\u201348.","DOI":"10.1145\/1379022.1375623"},{"key":"10.1016\/j.cl.2016.01.005_bib21","doi-asserted-by":"crossref","unstructured":"Jeannet Bertrand, Min\u00e9 Antoine. Apron: a library of numerical abstract domains for static analysis. In: Computer aided verification (CAV); 2009. p. 661\u20137.","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"10.1016\/j.cl.2016.01.005_bib22","doi-asserted-by":"crossref","unstructured":"Jhala Ranjit, McMillan Kenneth L. Array abstraction from proofs. In: Computer aided verification (CAV); 2007. p. 193\u2013206.","DOI":"10.1007\/978-3-540-73368-3_23"},{"key":"10.1016\/j.cl.2016.01.005_bib23","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs Laura, Voronkov Andrei. Finding loop invariants for programs over array using a theorem prover. In: Fundamental approaches to software engineering (FASE); 2009. p. 470\u201385.","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"10.1016\/j.cl.2016.01.005_bib24","doi-asserted-by":"crossref","unstructured":"Liu Jiangchao, Rival Xavier. Abstraction of arrays based on non contiguous partitions. In: Verification, model checking, and abstract interpretation (VMCAI); 2015. p. 282\u201399.","DOI":"10.1007\/978-3-662-46081-8_16"},{"key":"10.1016\/j.cl.2016.01.005_bib25","doi-asserted-by":"crossref","unstructured":"McMillan Kenneth L. Quantified invariant generation using an interpolation saturation prover. In: Tools and algorithms for the construction and analysis of systems (TACAS); 2008. p. 413\u201327.","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"10.1016\/j.cl.2016.01.005_bib26","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"Higher-Order Symbol. Comput."},{"key":"10.1016\/j.cl.2016.01.005_bib27","doi-asserted-by":"crossref","unstructured":"Palix Nicolas, Thomas Ga\u00ebl, Saha Suman, Calv\u00e8s Christophe, Lawall Julia L, Muller Gilles. Faults in linux: ten years later. In: Architectural support for programming languages and operating systems (ASPLOS); 2011. p. 305\u201318.","DOI":"10.1145\/1961296.1950401"},{"key":"10.1016\/j.cl.2016.01.005_bib28","unstructured":"Scott Dana. Outline of a mathematical theory of computation. Oxford University Computing Laboratory, Programming Research Group, oxford; 1970."},{"key":"10.1016\/j.cl.2016.01.005_bib29","doi-asserted-by":"crossref","unstructured":"Seghir Mohamed Nassim, Podelski Andreas, Wies Thomas. Abstraction refinement for quantified array assertions. In: Static analysis symposium (SAS); 2009. p. 3\u201318.","DOI":"10.1007\/978-3-642-03237-0_3"},{"key":"10.1016\/j.cl.2016.01.005_bib30","doi-asserted-by":"crossref","unstructured":"Sotin Pascal, Rival Xavier. Hierarchical shape abstraction of dynamic structures in static blocks. In: Asian symposium on programming languages and systems (APLAS); 2012. p. 131\u201347.","DOI":"10.1007\/978-3-642-35182-2_10"},{"key":"10.1016\/j.cl.2016.01.005_bib31","volume":"vol. 2","author":"Tanenbaum","year":"1987"},{"key":"10.1016\/j.cl.2016.01.005_bib32","doi-asserted-by":"crossref","unstructured":"Toubhans Antoine, Evan Chang Bor-Yuh, Rival Xavier. Reduced product combination of abstract domains for shapes. In: Verification, model checking, and abstract interpretation (VMCAI); 2013. p. 375\u201395.","DOI":"10.1007\/978-3-642-35873-9_23"},{"key":"10.1016\/j.cl.2016.01.005_bib33","doi-asserted-by":"crossref","unstructured":"Yang Hongseok, Lee Oukseh, Berdine Josh, Calcagno Cristiano, Cook Byron, Distefano Dino, et al. Scalable shape analysis for systems code. In: Computer aided verification (CAV); 2008. p. 385\u201398.","DOI":"10.1007\/978-3-540-70545-1_36"}],"container-title":["Computer Languages, Systems & Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842416000063?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842416000063?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T22:58:24Z","timestamp":1567551504000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1477842416000063"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":33,"alternative-id":["S1477842416000063"],"URL":"https:\/\/doi.org\/10.1016\/j.cl.2016.01.005","relation":{},"ISSN":["1477-8424"],"issn-type":[{"value":"1477-8424","type":"print"}],"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"An array content static analysis based on non-contiguous partitions","name":"articletitle","label":"Article Title"},{"value":"Computer Languages, Systems & Structures","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.cl.2016.01.005","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2016 Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}]}}