{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:46:42Z","timestamp":1777348002858,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T00:00:00Z","timestamp":1619222400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T00:00:00Z","timestamp":1619222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1007\/s10703-021-00366-4","type":"journal-article","created":{"date-parts":[[2021,4,25]],"date-time":"2021-04-25T07:11:32Z","timestamp":1619334692000},"page":"343-400","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A relational shape abstract domain"],"prefix":"10.1007","volume":"57","author":[{"given":"Hugo","family":"Illous","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1081-0467","authenticated-orcid":false,"given":"Matthieu","family":"Lemerre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,24]]},"reference":[{"key":"366_CR1","doi-asserted-by":"crossref","unstructured":"Amit D, Rinetzky N, Reps T, Sagiv M, Yahav E (2007) Comparison under abstraction for verifying linearizability. In: Conference on computer aided verification (CAV). Springer, Berlin, pp 477\u2013490","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"366_CR2","unstructured":"Baudin P, Filli\u00e2tre J-C, March\u00e9 C, Monate B, Moy Y, Prevosto V (2008) ACSL: ANSI C specification language"},{"key":"366_CR3","doi-asserted-by":"crossref","unstructured":"Bengtson J, Jensen JB, Birkedal L (2012) Charge! a framework for higher-order separation logic in coq. In: International conference on interactive theorem proving (ITP). Springer, Berlin, pp 315\u2013331","DOI":"10.1007\/978-3-642-32347-8_21"},{"key":"366_CR4","doi-asserted-by":"crossref","unstructured":"Blanchard A, Kosmatov N, Loulergue F (2018) Ghosts for lists: a critical module of contiki verified in frama-c. In: NASA formal methods symposium (NFM). Springer, Berlin","DOI":"10.1007\/978-3-319-77935-5_3"},{"key":"366_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Dr\u0103goi C, Enea C, Rezine A, Sighireanu M (2010) Invariant synthesis for programs manipulating lists with unbounded data. In: Conference on computer aided verification (CAV). Springer, pp 72\u201388","DOI":"10.1007\/978-3-642-14295-6_8"},{"key":"366_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Dragoi C, Enea C, Sighireanu M (2011) On inter-procedural analysis of programs with lists and data. In: Conference on programming language design and implementation (PLDI). ACM, pp 578\u2013589","DOI":"10.1145\/1993316.1993566"},{"key":"366_CR7","doi-asserted-by":"crossref","unstructured":"Calcagno C, Distefano D, O\u2019Hearn P, Yang H (2007) Footprint analysis: a shape analysis that discovers preconditions. In: Static analysis symposium (SAS). Springer, Berlin, pp 402\u2013418","DOI":"10.1007\/978-3-540-74061-2_25"},{"key":"366_CR8","doi-asserted-by":"crossref","unstructured":"Calcagno C, Distefano D, O\u2019Hearn P, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: Symposium on principles of programming languages (POPL). ACM, pp 289\u2013300","DOI":"10.1145\/1594834.1480917"},{"key":"366_CR9","doi-asserted-by":"crossref","unstructured":"Castelnuovo G, Naik M, Rinetzky N, Sagiv M, Yang H (2015) Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis. In: Static analysis symposium (SAS). Springer, Berlin, pp 252\u2013274","DOI":"10.1007\/978-3-662-48288-9_15"},{"key":"366_CR10","doi-asserted-by":"crossref","unstructured":"Chang B-YE, Rival X (2008) Relational inductive shape analysis. In: Symposium on principles of programming languages (POPL). ACM, pp 247\u2013260","DOI":"10.1145\/1328897.1328469"},{"key":"366_CR11","doi-asserted-by":"crossref","unstructured":"Chang B-YE, Rival X (2013) Modular construction of shape-numeric analyzers. In: Electronic proceedings in theoretical computer science. OPA, pp 161\u2013185","DOI":"10.4204\/EPTCS.129.11"},{"key":"366_CR12","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud A, Pottier F (2017) Temporary read-only permissions for separation logic. In: European symposium on programming (ESOP). Springer, pp 260\u2013286","DOI":"10.1007\/978-3-662-54434-1_10"},{"key":"366_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee R, Ryder BG, Landi WA (1999) Relevant context inference. In: Symposium on principles of programming languages (POPL). ACM, pp 133\u2013146","DOI":"10.1145\/292540.292554"},{"key":"366_CR14","doi-asserted-by":"crossref","unstructured":"Costea A, Sharma A, David C (2014) Hipimm: verifying granular immutability guarantees. In: Workshop on partial evaluation and program manipulation (PEPM), New York, NY, USA. ACM, pp 189\u2013193","DOI":"10.1145\/2543728.2543743"},{"key":"366_CR15","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Symposium on principles of programming languages (POPL). ACM, pp 84\u201397","DOI":"10.1145\/512760.512770"},{"key":"366_CR16","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Proceedings of the 2nd international symposium on programming, Paris, France. Dunod","DOI":"10.1145\/390018.808314"},{"key":"366_CR17","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symposium on principles of programming languages (POPL)","DOI":"10.1145\/512950.512973"},{"key":"366_CR18","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: Symposium on principles of programming languages (POPL). ACM","DOI":"10.1145\/567752.567778"},{"key":"366_CR19","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (2002) Modular static program analysis. In: Conference on compiler construction (cc). Springer, Berlin, pp 159\u2013179","DOI":"10.1007\/3-540-45937-5_13"},{"key":"366_CR20","doi-asserted-by":"crossref","unstructured":"Cox A, Chang B-YE, Rival X (2015) Desynchronized multi-state abstractions for open programs in dynamic languages. In: European symposium on programming (esoP). Springer, Berlin, pp 483\u2013509","DOI":"10.1007\/978-3-662-46669-8_20"},{"key":"366_CR21","doi-asserted-by":"crossref","unstructured":"David C, Chin W-N (2011) Immutable specifications for more concise and precise verification. In: Conference on object oriented programming systems languages and applications (OOPSLA), New York, NY, USA. ACM, pp 359\u2013374","DOI":"10.1145\/2076021.2048096"},{"key":"366_CR22","doi-asserted-by":"crossref","unstructured":"Dillig I, Dillig T, Aiken A, Sagiv M (2011) Precise and compact modular procedure summaries for heap manipulating programs. In: Conference on programming language design and implementation (PLDI). ACM, pp 567\u2013577","DOI":"10.1145\/1993316.1993565"},{"key":"366_CR23","doi-asserted-by":"crossref","unstructured":"Distefano D, Katoen J-P, Rensik A (2004) Who is pointing when to whom? In: Foundations of software technology and theoretical (FSTTCS). Springer, Berlin, pp 250\u2013262","DOI":"10.1007\/978-3-540-30538-5_21"},{"key":"366_CR24","doi-asserted-by":"crossref","unstructured":"Distefano D, Katoen J-P, Rensik A (2005) Safety and liveness in concurrent pointer programs. In: Formal methods for components and objects (FMCO). Springer, Berlin, pp 280\u2013312","DOI":"10.1007\/11804192_14"},{"key":"366_CR25","doi-asserted-by":"crossref","unstructured":"Distefano D, O\u2019Hearn P, Yang H (2006) A local shape analysis based on separation logic. In: Conference on tools and algorithms for the construction and analysis of systems (TACAS). Springer, Berlin, pp 287\u2013302","DOI":"10.1007\/11691372_19"},{"key":"366_CR26","doi-asserted-by":"crossref","unstructured":"Dunkels A, Gronvall B, Voigt T (2004) Contiki\u2014a lightweight and flexible operating system for tiny networked sensors. In: 29th annual IEEE international conference on local computer networks, 2004. IEEE, pp 455\u2013462","DOI":"10.1109\/LCN.2004.38"},{"key":"366_CR27","doi-asserted-by":"crossref","unstructured":"Fu M, Li Y, Feng X, Shao Z, Zhang Y (2010) Reasoning about optimistic concurrency using a program logic for history. In: International conference on concurrency theory (ICC). Springer, Berlin, pp 388\u2013402","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"366_CR28","doi-asserted-by":"crossref","unstructured":"Gulavani BS, Chakraborty S, Ramalingam G, Nori AV (2009) Bottom-up shape analysis. In: Static analysis symposium (SAS). Springer, Berlin, pp 188\u2013204","DOI":"10.1007\/978-3-642-03237-0_14"},{"key":"366_CR29","unstructured":"Jacobs B, Piessens F (2008) The verifast program verifier. Technical report, Department of Computer Science, KU Leuven, Belgium"},{"issue":"2","key":"366_CR30","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1667048.1667050","volume":"32","author":"Bertrand Jeannet","year":"2010","unstructured":"Jeannet Bertrand, Loginov Alexey, Reps Thomas, Sagiv Mooly (2010) A relational approach to interprocedural shape analysis. ACM Trans Program Lang Syst (TOPLAS) 32(2):5","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"366_CR31","doi-asserted-by":"crossref","unstructured":"Kaki G, Jagannathan S (2014) A relational framework for higher-order shape analysis. In: International conference on functional programming (ICFP). ACM, pp 311\u2013324","DOI":"10.1145\/2692915.2628159"},{"issue":"3","key":"366_CR32","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"Florent Kirchner","year":"2015","unstructured":"Kirchner Florent, Kosmatov Nikolai, Prevosto Virgile, Signoles Julien, Yakobowski Boris (2015) Frama-c: A software analysis perspective. Formal Aspects Comput 27(3):573\u2013609","journal-title":"Formal Aspects Comput"},{"key":"366_CR33","doi-asserted-by":"crossref","unstructured":"Le QL, Gherghina C, Qin S, Chin W-N (2014) Shape analysis via second-order bi-abduction. In: Conference on computer aided verification (CAV). Springer, Berlin, pp 52\u201368","DOI":"10.1007\/978-3-319-08867-9_4"},{"key":"366_CR34","unstructured":"Leavens GT, Baker AL, Ruby C (1998) Jml: a java modeling language. In: Formal underpinnings of java workshop (at OOPSLA\u201998), pp 404\u2013420"},{"key":"366_CR35","doi-asserted-by":"crossref","unstructured":"Li H, Berenger F, Chang B-YE, Rival X (2017) Semantic-directed clumping of disjunctive abstract states. In: Symposium on principles of programming languages (POPL). ACM, vol\u00a052, pp 32\u201345","DOI":"10.1145\/3093333.3009881"},{"key":"366_CR36","doi-asserted-by":"crossref","unstructured":"Nguyen HH, David C, Qin S, Chin W-N (2007) Automated verification of shape and size properties via separation logic. In: Conference on verification, model checking, and abstract interpretation (VMCAI). Springer, Berlin, pp 251\u2013266","DOI":"10.1007\/978-3-540-69738-1_18"},{"issue":"1\u20133","key":"366_CR37","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"Peter\u00a0W O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn Peter\u00a0W (2007) Resources, concurrency, and local reasoning. Theor Comput Sci 375(1\u20133):271\u2013307","journal-title":"Theor Comput Sci"},{"key":"366_CR38","doi-asserted-by":"crossref","unstructured":"Popeea C, Chin W-N (2006) Inferring disjunctive postconditions. In: Conference on advances in computer science: secure software and related issues. Springer, Berlin, pp 331\u2013345","DOI":"10.1007\/978-3-540-77505-8_26"},{"key":"366_CR39","doi-asserted-by":"crossref","unstructured":"Reynolds J (2002) Separation logic: a logic for shared mutable data structures. In: Symposium on logics in computer science (LICS). IEEE, pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"366_CR40","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"Mooly Sagiv","year":"2002","unstructured":"Sagiv Mooly, Reps Thomas, Wilhelm Reinhard (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst (TOPLAS) 24(3):217\u2013298","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"issue":"1","key":"366_CR41","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10515-006-0005-x","volume":"14","author":"Mana Taghdiri","year":"2007","unstructured":"Taghdiri Mana, Jackson Daniel (2007) Inferring specifications to detect errors in code. Autom Softw Eng (ASE) 14(1):87\u2013121","journal-title":"Autom Softw Eng (ASE)"},{"key":"366_CR42","doi-asserted-by":"crossref","unstructured":"Yahav E, Reps T, Sagiv M, Wilhelm R (2003) Verifying temporal heap properties specified via evolution logic. In: European symposium on programming (ESOP). Springer, Berlin, pp 204\u2013222","DOI":"10.1007\/3-540-36575-3_15"},{"key":"366_CR43","doi-asserted-by":"crossref","unstructured":"Zhu H, Petri G, Jagannathan S (2016) Automatically learning shape specifications. In: Conference on programming language design and implementation (PLDI). ACM, pp 491\u2013507","DOI":"10.1145\/2980983.2908125"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00366-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00366-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00366-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,25]],"date-time":"2022-12-25T11:04:50Z","timestamp":1671966290000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00366-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,24]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["366"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00366-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4,24]]},"assertion":[{"value":"25 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 April 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}