{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:18:08Z","timestamp":1791299888647,"version":"4.1.0"},"reference-count":100,"publisher":"Emerald","issue":"1-2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,10,5]]},"abstract":"<jats:p>The computation of semantic information about the behavior of pointer-manipulating programs has been a long standing issue, attacked with diverse and numerous techniques and tools for over 50 years. As usual in automatic verification of infinite-state programs, properties of interest are not computable. Thus, static analyses can only be conservative, leading different analyses to make different tradeoffs between the intricacies of the properties they detect, the precision of their inference procedure and analysis, and the scalability of the analysis.<\/jats:p>\n                  <jats:p>In this context, shape analyses focus on inferring highly complex properties of heap-manipulating programs. These programs utilize data structures which are implemented using an unbounded number of dynamically- (heap-) allocated memory cells interconnected via mutable pointer-links. Because shape analyses have to reason about data structures whose size is not bounded by a fixed, known value, they cannot track explicitly the particular properties of every concrete memory cell which the program uses, as done, e.g., by analysis of variable-manipulating non-recursive programs. Instead, shape analyses summarize memory regions by letting one piece of abstract information, called summary predicate, describe several concrete cells. The need to cope with data structures of unbounded sizes is a challenge shape analyses share with static analyzers of array-manipulating programs. However, while the size of an array may change in different executions, its layout (i.e., its dimensions and the way its contents are spread over the memory) is fixed. In contrast, the layout of a pointer-linked data structure, colloquially referred to as its shape, may evolve dynamically during the program execution and a memory cell can be part of different data structures at different points in time. As a result, shape analyses need to let the denotation of summary predicates in terms of the constituents and layouts of the memory regions which they represent evolve during the analysis as well.<\/jats:p>\n                  <jats:p>In this survey, we consider that shape analyses are characterized and defined by the presence of summary predicates describing a set of concrete memory cells that varies during the course of the analysis. We use this characterization as a means for distinguishing shape analyses as a particular class of pointer analyses. We show that many \u201cstandard\u201d pointer analyses do not fit the aforementioned description, while many analyses relying on very different mathematical foundations, e.g., shape graphs, three-valued logic, and separation logic, do.<\/jats:p>\n                  <jats:p>The ambition of this survey is to provide a comprehensive introduction to the field of shape analysis, and to present the foundation of this topic, in a single document that is accessible to readers who are not familiar with it. To do so, we characterize the essence of shape analysis compared to more classical pointer analyses. We supply the intuition underlying the abstractions commonly used in shape analysis and the algorithms that allow to statically compute intricate semantic properties. Then, we cover the main families of shape analysis abstraction and algorithms, highlight the similarities between them, and also characterize the main differences between the most common approaches. Last, we review a few other static analysis works (such as array abstractions, dictionary abstractions and interprocedural analyses) that were influenced by the ideas of shape analysis, so as to demonstrate the impact of the field.<\/jats:p>","DOI":"10.1561\/2500000037","type":"journal-article","created":{"date-parts":[[2020,10,5]],"date-time":"2020-10-05T09:31:25Z","timestamp":1601890285000},"page":"1-158","source":"Crossref","is-referenced-by-count":11,"title":["Shape Analysis"],"prefix":"10.1108","volume":"6","author":[{"given":"Bor-Yuh Evan","family":"Chang","sequence":"first","affiliation":[{"name":"University of Colorado ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cezara","family":"Dr\u0103goi","sequence":"additional","affiliation":[{"name":"INRIA, France and CNRS, PSL University ,","place":["France"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roman","family":"Manevich","sequence":"additional","affiliation":[{"name":"Ben-Gurion University of the Negev ,","place":["Israel"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University ,","place":["Israel"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[{"name":"INRIA, France and CNRS, PSL University ,","place":["France"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"140","published-online":{"date-parts":[[2020,10,5]]},"reference":[{"issue":"4","key":"2026032910224899000_ref001","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/s00236-015-0235-0","article-title":"Verification of heap manipulating programs with ordered data by extended forest automata","volume":"53","author":"Abdulla","year":"2016","journal-title":"Acta Informatica"},{"key":"2026032910224899000_ref002","volume-title":"Program analysis and specialization for the C programming language","author":"Andersen","year":"1994"},{"key":"2026032910224899000_ref003","first-page":"91","article-title":"Shape analysis of single-parent heaps","author":"Balaban","year":"2007"},{"key":"2026032910224899000_ref004","first-page":"115","article-title":"Smallfoot: Modular automatic assertion checking with separation logic","author":"Berdine","year":"2005"},{"key":"2026032910224899000_ref005","first-page":"52","volume-title":"APLAS","author":"Berdine","year":"2005"},{"key":"2026032910224899000_ref006","first-page":"178","article-title":"Shape analysis for composite data structures","author":"Berdine","year":"2007"},{"key":"2026032910224899000_ref007","first-page":"399","article-title":"Thread quantification for concurrent shape analysis","author":"Berdine","year":"2008"},{"key":"2026032910224899000_ref008","first-page":"178","article-title":"Slayer: Memory safety for systems-level code","author":"Berdine","year":"2011"},{"key":"2026032910224899000_ref009","first-page":"517","article-title":"Programs with lists are counter automata","author":"Bouajjani","year":"2006"},{"key":"2026032910224899000_ref010","first-page":"578","article-title":"On inter-procedural analysis of programs with lists and data","volume-title":"Conference on Programming Languages Design and Implementation (PLDI)","author":"Bouajjani","year":"2011"},{"key":"2026032910224899000_ref011","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-27940-9_1","article-title":"Abstract domains for automated reasoning about list-manipulating programs with infinite data","volume-title":"Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"Bouajjani","year":"2012"},{"key":"2026032910224899000_ref012","first-page":"66","article-title":"Learning shape analysis","author":"Brockschmidt","year":"2017"},{"key":"2026032910224899000_ref013","first-page":"459","article-title":"Infer: An automatic program verifier for memory safety of C programs","author":"Calcagno","year":"2011"},{"key":"2026032910224899000_ref014","first-page":"182","article-title":"Beyond reachability: Shape abstraction in the presence of pointer arithmetic","author":"Calcagno","year":"2006"},{"key":"2026032910224899000_ref015","first-page":"402","article-title":"Footprint analysis: A shape analysis that discovers preconditions","author":"Calcagno","year":"2007"},{"key":"2026032910224899000_ref016","first-page":"289","article-title":"Compositional shape analysis by means of bi-abduction","author":"Calcagno","year":"2009"},{"key":"2026032910224899000_ref017","first-page":"247","article-title":"Relational inductive shape analysis","author":"Chang","year":"2008"},{"key":"2026032910224899000_ref018","first-page":"161","article-title":"Modular construction of shape-numeric analyzers","author":"Chang","year":"2013"},{"key":"2026032910224899000_ref019","first-page":"384","article-title":"Shape analysis with structural invariant checkers","author":"Chang","year":"2007"},{"key":"2026032910224899000_ref020","first-page":"296","article-title":"Analysis of pointers and structures","author":"Chase","year":"1990"},{"key":"2026032910224899000_ref021","first-page":"307","article-title":"Automated verification of shape, size and bag properties","author":"Chin","year":"2007"},{"key":"2026032910224899000_ref022","first-page":"49","article-title":"Fast interprocedural alias analysis","author":"Cooper","year":"1989"},{"key":"2026032910224899000_ref023","first-page":"238","article-title":"Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"key":"2026032910224899000_ref024","first-page":"269","article-title":"Systematic design of program analysis frameworks","volume-title":"Symposium on Principles of Programming Languages (POPL)","author":"Cousot","year":"1979"},{"key":"2026032910224899000_ref025","first-page":"84","article-title":"Automatic discovery of linear restraints among variables of a program","author":"Cousot","year":"1978"},{"key":"2026032910224899000_ref026","first-page":"105","article-title":"A parametric segmentation functor for fully automatic and scalable array content analysis","author":"Cousot","year":"2011"},{"key":"2026032910224899000_ref027","first-page":"134","article-title":"Automatic analysis of open objects in dynamic language programs","author":"Cox","year":"2014"},{"key":"2026032910224899000_ref028","first-page":"483","article-title":"Desynchronized multistate abstractions for open programs in dynamic languages","author":"Cox","year":"2015"},{"key":"2026032910224899000_ref029","first-page":"230","article-title":"Interprocedural may-alias analysis for pointers: Beyond k-limiting","author":"Deutsch","year":"1994"},{"key":"2026032910224899000_ref030","first-page":"187","article-title":"Precise reasoning for programs using containers","author":"Dillig","year":"2011"},{"key":"2026032910224899000_ref031","first-page":"287","article-title":"A local shape analysis based on separation logic","author":"Distefano","year":"2006"},{"key":"2026032910224899000_ref032","first-page":"82","article-title":"Automatic verification of strongly dynamic software systems","author":"Dor","year":"2005"},{"key":"2026032910224899000_ref033","first-page":"372","article-title":"Predator: A practical tool for checking manipulation of dynamic data structures using separation logic","author":"Dudka","year":"2011"},{"key":"2026032910224899000_ref034","first-page":"1","article-title":"Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C","volume-title":"Symposium on Principles of Programming Languages (POPL)","author":"Ghiya","year":"1996"},{"key":"2026032910224899000_ref035","first-page":"240","article-title":"Interprocedural shape analysis with separated heap abstractions","author":"Gotsman","year":"2006"},{"key":"2026032910224899000_ref036","first-page":"72","article-title":"Construction of abstract state graphs with PVS","author":"Graf","year":"1997"},{"key":"2026032910224899000_ref037","first-page":"350","article-title":"Automata-based verification of programs with tree updates","volume-title":"Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Habermehl","year":"2006"},{"key":"2026032910224899000_ref038","first-page":"424","article-title":"Forest automata for verification of heap manipulation","author":"Habermehl","year":"2011"},{"issue":"1","key":"2026032910224899000_ref039","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/s10703-012-0150-8","article-title":"Forest automata for verification of heap manipulation","volume":"41","author":"Habermehl","year":"2012","journal-title":"Formal Methods in System Design (FMSD)"},{"key":"2026032910224899000_ref040","first-page":"339","article-title":"Discovering properties about arrays in simple programs","author":"Halbwachs","year":"2008"},{"key":"2026032910224899000_ref041","first-page":"740","article-title":"Fully automated shape analysis based on forest automata","author":"Hol\u00edk","year":"2013"},{"key":"2026032910224899000_ref042","first-page":"212","article-title":"A relational shape abstract domain","author":"Illous","year":"2017"},{"key":"2026032910224899000_ref043","first-page":"201","article-title":"Deciding entailments in inductive separation logic with tree automata","author":"Iosif","year":"2014"},{"key":"2026032910224899000_ref044","first-page":"14","article-title":"BI as an assertion language for mutable data structures","author":"Ishtiaq","year":"2001"},{"key":"2026032910224899000_ref045","first-page":"756","article-title":"Effectively-propositional reasoning about reachability in linked data structures","author":"Itzhaky","year":"2013"},{"key":"2026032910224899000_ref046","first-page":"246","article-title":"A relational approach to interprocedural shape analysis","author":"Jeannet","year":"2004"},{"issue":"2","key":"2026032910224899000_ref047","doi-asserted-by":"crossref","first-page":"5:1","DOI":"10.1145\/1667048.1667050","article-title":"A relational approach to interprocedural shape analysis","volume":"32","author":"Jeannet","year":"2010","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2026032910224899000_ref048","first-page":"244","article-title":"Flow analysis and optimization of LISP-like structures","author":"Jones","year":"1979"},{"key":"2026032910224899000_ref049","first-page":"66","article-title":"A flexible approach to interprocedural data flow analysis and programs with recursive data structures","author":"Jones","year":"1982"},{"key":"2026032910224899000_ref050","volume-title":"Abstract Storage Structures","author":"Jonkers","year":"1981"},{"key":"2026032910224899000_ref051","volume-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"2026032910224899000_ref052","first-page":"214","article-title":"Shape analysis of low-level C with overlapping structures","author":"Kreiker","year":"2010"},{"key":"2026032910224899000_ref053","first-page":"24","article-title":"Detecting conflicts between structure accesses","author":"Larus","year":"1988"},{"key":"2026032910224899000_ref054","first-page":"387","article-title":"Separating shape graphs","author":"Laviron","year":"2010"},{"key":"2026032910224899000_ref055","first-page":"382","article-title":"Satisfiability modulo heap-based programs","author":"Le","year":"2016"},{"key":"2026032910224899000_ref056","first-page":"592","article-title":"Program analysis for overlaid data structures","author":"Lee","year":"2011"},{"key":"2026032910224899000_ref057","first-page":"280","article-title":"TVLA: A system for implementing static analyses","author":"Lev-Ami","year":"2000"},{"key":"2026032910224899000_ref058","first-page":"90","article-title":"Shape analysis for unstructured sharing","author":"Li","year":"2015"},{"key":"2026032910224899000_ref059","first-page":"32","article-title":"Semantic-directed clumping of disjunctive abstract states","author":"Li","year":"2017"},{"key":"2026032910224899000_ref060","first-page":"282","article-title":"Abstraction of arrays based on non contiguous partitions","author":"Liu","year":"2015"},{"key":"2026032910224899000_ref061","doi-asserted-by":"crossref","DOI":"10.1109\/TCAD.2018.2858462","article-title":"Automatic verification of embedded system code manipulating dynamic structures stored in contiguous regions","author":"Liu","year":"2018"},{"key":"2026032910224899000_ref062","first-page":"519","article-title":"Abstraction refinement via inductive learning","author":"Loginov","year":"2005"},{"key":"2026032910224899000_ref063","first-page":"611","article-title":"Decidable logics combining heap structures and data","author":"Madhusudan","year":"2011"},{"key":"2026032910224899000_ref064","first-page":"419","article-title":"Arithmetic strengthening for shape analysis","author":"Magill","year":"2007"},{"key":"2026032910224899000_ref065","first-page":"211","article-title":"Automatic numeric abstractions for heap-manipulating programs","author":"Magill","year":"2010"},{"key":"2026032910224899000_ref066","first-page":"363","article-title":"Heap decomposition for concurrent shape analysis","author":"Manevich","year":"2008"},{"key":"2026032910224899000_ref067","first-page":"426","article-title":"From shape analysis to termination analysis in linear time","author":"Manevich","year":"2016"},{"key":"2026032910224899000_ref068","first-page":"263","article-title":"Shape analysis in the absence of pointers and structure","author":"Might","year":"2010"},{"key":"2026032910224899000_ref069","first-page":"54","article-title":"Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics","author":"Min\u00e9","year":"2006"},{"key":"2026032910224899000_ref070","first-page":"38","article-title":"Verifying reachability invariants of linked structures","author":"Nelson","year":"1983"},{"issue":"2","key":"2026032910224899000_ref071","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","article-title":"The logic of bunched implications","volume":"5","author":"O\u2019Hearn","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"2026032910224899000_ref072","first-page":"1","article-title":"Local reasoning about programs that alter data structures","author":"O\u2019Hearn","year":"2001"},{"key":"2026032910224899000_ref073","first-page":"440","article-title":"Natural proofs for data structure manipulation in C using separation logic","author":"Pek","year":"2014"},{"key":"2026032910224899000_ref074","first-page":"773","article-title":"Automating separation logic using SMT","author":"Piskac","year":"2013"},{"key":"2026032910224899000_ref075","first-page":"268","article-title":"Boolean heaps","author":"Podelski","year":"2005"},{"key":"2026032910224899000_ref076","first-page":"231","article-title":"Natural proofs for structure, data, and separation","author":"Qiu","year":"2013"},{"key":"2026032910224899000_ref077","first-page":"49","article-title":"Precise interprocedural dataflow analysis via graph reachability","author":"Reps","year":"1995"},{"key":"2026032910224899000_ref078","first-page":"380","article-title":"Finite differencing of logical formulas for static analysis","author":"Reps","year":"2003"},{"key":"2026032910224899000_ref079","first-page":"296","article-title":"Automatic computation of data set definitions","author":"Reynolds","year":"1968"},{"key":"2026032910224899000_ref080","first-page":"55","article-title":"Separation logic: A logic for shared mutable data structures","author":"Reynolds","year":"2002"},{"key":"2026032910224899000_ref081","first-page":"133","article-title":"Interprocedural shape analysis for recursive programs","author":"Rinetzky","year":"2001"},{"key":"2026032910224899000_ref082","first-page":"296","article-title":"A semantics for procedure local heaps and its abstractions","volume-title":"Symposium on Principles of Programming Languages (POPL)","author":"Rinetzky","year":"2005"},{"key":"2026032910224899000_ref083","first-page":"284","article-title":"Interprocedural shape analysis for cutpoint-free programs","author":"Rinetzky","year":"2005"},{"key":"2026032910224899000_ref084","first-page":"173","article-title":"Calling context abstraction with shapes","author":"Rival","year":"2011"},{"issue":"1","key":"2026032910224899000_ref085","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/271510.271517","article-title":"Solving shape-analysis problems in languages with destructive updating","volume":"20","author":"Sagiv","year":"1998","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2026032910224899000_ref086","first-page":"105","article-title":"Parametric shape analysis via 3-valued logic","volume-title":"Symposium on Principles of Programming Languages (POPL)","author":"Sagiv","year":"1999"},{"issue":"3","key":"2026032910224899000_ref087","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","article-title":"Parametric shape analysis via 3-valued logic","volume":"24","author":"Sagiv","year":"2002","journal-title":"Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"2026032910224899000_ref088","volume-title":"Program Flow Analysis: Theory and Applications","author":"Sharir","year":"1981"},{"key":"2026032910224899000_ref089","volume-title":"Control-flow analysis of higher-order languages","author":"Shivers","year":"1991"},{"issue":"1","key":"2026032910224899000_ref090","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1561\/2500000014","article-title":"Pointer analysis","volume":"2","author":"Smaragdakis","year":"2015","journal-title":"Found. Trends Program. Lang"},{"key":"2026032910224899000_ref091","first-page":"459","article-title":"Precise interprocedural analysis in the presence of pointers to the stack","author":"Sotin","year":"2011"},{"issue":"1","key":"2026032910224899000_ref092","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/j.entcs.2010.09.012","article-title":"Concrete memory models for shape analysis","volume":"267","author":"Sotin","year":"2010","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"2","key":"2026032910224899000_ref093","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1016\/j.artint.2010.10.006","article-title":"A new representation and associated algorithms for generalized planning","volume":"175","author":"Srivastava","year":"2011","journal-title":"Artificial Intelligence"},{"key":"2026032910224899000_ref094","first-page":"32","article-title":"Points-to analysis in almost linear time","author":"Steensgaard","year":"1996"},{"issue":"1","key":"2026032910224899000_ref095","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/0890-5401(92)90076-R","article-title":"A lattice for abstract interpretation of dynamic (LISP-like) structures","volume":"101","author":"Stransky","year":"1992","journal-title":"Inf. Comput."},{"key":"2026032910224899000_ref096","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/978-3-642-35873-9_23","article-title":"Reduced product combination of abstract domains for shapes","volume-title":"Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"Toubhans","year":"2013"},{"key":"2026032910224899000_ref097","first-page":"285","article-title":"An abstract domain combinator for separately conjoining memory abstractions","author":"Toubhans","year":"2014"},{"key":"2026032910224899000_ref098","first-page":"450","article-title":"Automatically proving linearizability","author":"Vafeiadis","year":"2010"},{"key":"2026032910224899000_ref099","first-page":"267","article-title":"Towards shape analysis for device drivers","author":"Yang","year":"2007"},{"key":"2026032910224899000_ref100","first-page":"385","article-title":"Scalable shape analysis for systems code","author":"Yang","year":"2008"}],"container-title":["Foundations and Trends\u00ae in Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/6\/1-2\/1\/11044421\/2500000037en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/6\/1-2\/1\/11044421\/2500000037en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:16:47Z","timestamp":1777486607000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftpgl\/article\/6\/1-2\/1\/1328329\/Shape-Analysis"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,5]]},"references-count":100,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2020,10,5]]}},"URL":"https:\/\/doi.org\/10.1561\/2500000037","relation":{},"ISSN":["2325-1107","2325-1131"],"issn-type":[{"value":"2325-1107","type":"print"},{"value":"2325-1131","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,10,5]]}}}