{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:09:59Z","timestamp":1767773399386,"version":"3.38.0"},"reference-count":31,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2012,5,1]],"date-time":"2012-05-01T00:00:00Z","timestamp":1335830400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"vor","delay-in-days":1461,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Computer and System Sciences"],"published-print":{"date-parts":[[2012,5]]},"DOI":"10.1016\/j.jcss.2011.08.003","type":"journal-article","created":{"date-parts":[[2011,8,16]],"date-time":"2011-08-16T17:12:16Z","timestamp":1313514736000},"page":"853-876","source":"Crossref","is-referenced-by-count":3,"title":["Verification of multi-linked heaps"],"prefix":"10.1016","volume":"78","author":[{"given":"Ittai","family":"Balaban","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Yaniv","family":"Sa\u02bcar","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jcss.2011.08.003_br0010","series-title":"Proc. 13rd Intl. Conference on Computer Aided Verification","first-page":"221","article-title":"Parameterized verification with automatically computed inductive assertions","volume":"vol. 2102","author":"Arons","year":"2001"},{"key":"10.1016\/j.jcss.2011.08.003_br0020","unstructured":"Ittai Balaban, Shape analysis by augmentation, abstraction, and transformation, PhD thesis, New York University, New York, May 2007."},{"key":"10.1016\/j.jcss.2011.08.003_br0030","series-title":"Proc. of the 6th Int. Conference on Verification, Model Checking, and Abstract Interpretation","first-page":"164","article-title":"Shape analysis by predicate abstraction","volume":"vol. 3385","author":"Balaban","year":"2005"},{"issue":"1","key":"10.1016\/j.jcss.2011.08.003_br0040","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1142\/S0129054107004553","article-title":"Modular ranking abstraction","volume":"18","author":"Balaban","year":"2007","journal-title":"Internat. J. Found. Comput. Sci."},{"key":"10.1016\/j.jcss.2011.08.003_br0050","doi-asserted-by":"crossref","unstructured":"Ittai Balaban, Amir Pnueli, Lenore D. Zuck, Shape analysis of single-parent heaps, in: Proc. of the 8th Int. Conference on Verification, Model Checking, and Abstract Interpretation, 2007, pp. 91\u2013105.","DOI":"10.1007\/978-3-540-69738-1_7"},{"key":"10.1016\/j.jcss.2011.08.003_br0060","doi-asserted-by":"crossref","unstructured":"Thomas Ball, Andreas Podelski, Sriram K. Rajamani, Relative completeness of abstraction refinement for software model checking, in: Tools and Algorithms for Construction and Analysis of Systems, 2002, pp. 158\u2013172.","DOI":"10.1007\/3-540-46002-0_12"},{"key":"10.1016\/j.jcss.2011.08.003_br0070","doi-asserted-by":"crossref","unstructured":"Thomas Ball, Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, in: Lecture Notes in Comput. Sci., vol. 2057, 2001, pp. 103\u2013122.","DOI":"10.1007\/3-540-45139-0_7"},{"key":"10.1016\/j.jcss.2011.08.003_br0080","doi-asserted-by":"crossref","unstructured":"Michael Benedikt, Thomas W. Reps, Shmuel Sagiv, A decidable logic for describing linked data structures, in: ESOP, 1999, pp. 2\u201319.","DOI":"10.1007\/3-540-49099-X_2"},{"key":"10.1016\/j.jcss.2011.08.003_br0090","doi-asserted-by":"crossref","unstructured":"Josh Berdine, Byron Cook, Dino Distefano, Peter W. O\u02bcHearn, Automatic termination proofs for programs with shape-shifting heaps, in: CAV, 2006, pp. 386\u2013400.","DOI":"10.1007\/11817963_35"},{"key":"10.1016\/j.jcss.2011.08.003_br0100","doi-asserted-by":"crossref","unstructured":"Jesse D. Bingham, Zvonimir Rakamaric, A logic and decision procedure for predicate abstraction of heap-manipulating programs, in: VMCAI, 2006, pp. 207\u2013221.","DOI":"10.1007\/11609773_14"},{"key":"10.1016\/j.jcss.2011.08.003_br0110","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","article-title":"The Classical Decision Problem","author":"B\u00f6rger","year":"1997"},{"key":"10.1016\/j.jcss.2011.08.003_br0120","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tom\u00e1s Vojnar, Programs with lists are counter automata, in: CAV, 2006, pp. 517\u2013531.","DOI":"10.1007\/11817963_47"},{"key":"10.1016\/j.jcss.2011.08.003_br0130","series-title":"CONCUR","first-page":"178","article-title":"A logic-based framework for reasoning about composite data structures","volume":"vol. 5710","author":"Bouajjani","year":"2009"},{"key":"10.1016\/j.jcss.2011.08.003_br0140","series-title":"Proc. IBM Workshop on Logics of Programs","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","volume":"vol. 131","author":"Clarke","year":"1981"},{"key":"10.1016\/j.jcss.2011.08.003_br0150","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith, Counterexample-guided abstraction refinement, in: Computer Aided Verification, 2000, pp. 154\u2013169.","DOI":"10.1007\/10722167_15"},{"key":"10.1016\/j.jcss.2011.08.003_br0160","first-page":"169","article-title":"Characterizing correctness properties of parallel programs using fixpoints","volume":"vol. 85","author":"Emerson","year":"1980"},{"key":"10.1016\/j.jcss.2011.08.003_br0170","doi-asserted-by":"crossref","unstructured":"Erich Gr\u00e4del, Martin Otto, Eric Rosen, Undecidability results on two-variable logics, in: STACS, 1997, pp. 249\u2013260.","DOI":"10.1007\/BFb0023464"},{"key":"10.1016\/j.jcss.2011.08.003_br0180","series-title":"POPL","first-page":"239","article-title":"A combination framework for tracking partition sizes","author":"Gulwani","year":"2009"},{"key":"10.1016\/j.jcss.2011.08.003_br0190","doi-asserted-by":"crossref","unstructured":"Neil Immerman, Alexander M. Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh, The boundary between decidability and undecidability for transitive-closure logics, in: CSL, 2004, pp. 160\u2013174.","DOI":"10.1007\/978-3-540-30124-0_15"},{"key":"10.1016\/j.jcss.2011.08.003_br0200","series-title":"Proc. 16th Intl. Conference on Computer Aided Verification","first-page":"281","article-title":"Verification via structure simulation","author":"Immerman","year":"2004"},{"key":"10.1016\/j.jcss.2011.08.003_br0210","series-title":"Program Flow Analysis: Theory and Applications, Chapter 4","first-page":"102","article-title":"Flow analysis and optimization of Lisp-like structures","author":"Jones","year":"1981"},{"issue":"1","key":"10.1016\/j.jcss.2011.08.003_br0220","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1006\/inco.2000.3000","article-title":"Verification by augmented finitary abstraction","volume":"163","author":"Kesten","year":"2000","journal-title":"Inform. and Comput."},{"key":"10.1016\/j.jcss.2011.08.003_br0230","series-title":"Proc. 20th ACM Symp. Princ. of Prog. Lang.","first-page":"196","article-title":"Graph types","author":"Klarlund","year":"1993"},{"key":"10.1016\/j.jcss.2011.08.003_br0240","series-title":"Proc. of the 6th Int. Conference on Verification, Model Checking, and Abstract Interpretation","first-page":"181","article-title":"Predicate abstraction and canonical abstraction for singly-linked lists","volume":"vol. 3385","author":"Manevich","year":"2005"},{"key":"10.1016\/j.jcss.2011.08.003_br0250","doi-asserted-by":"crossref","unstructured":"Anders M\u00f8ller, Michael I. Schwartzbach, The pointer assertion logic engine, in: Programming Language Design and Implementation, 2001.","DOI":"10.1145\/381694.378851"},{"key":"10.1016\/j.jcss.2011.08.003_br0260","series-title":"Proc. 22nd Intl. Conference on Computer Aided Verification","first-page":"171","article-title":"JTLV: A framework for developing verification algorithms","volume":"vol. 6174","author":"Pnueli","year":"2010"},{"key":"10.1016\/j.jcss.2011.08.003_br0270","unstructured":"Andreas Podelski, Private communication, January 2010."},{"key":"10.1016\/j.jcss.2011.08.003_br0280","doi-asserted-by":"crossref","unstructured":"John C. Reynolds, Separation logic: A logic for shared mutable data structures, in: LICS, 2002, pp. 55\u201374.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"10.1016\/j.jcss.2011.08.003_br0290","series-title":"Proc. 9th International Conference on Computer Aided Verification (CAV\u02bc97), vol. 1254","first-page":"72","article-title":"Construction of abstract state graphs with PVS","author":"Graf","year":"1997"},{"key":"10.1016\/j.jcss.2011.08.003_br0300","doi-asserted-by":"crossref","unstructured":"Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, Martin C. Rinard, Field constraint analysis, in: Proc. of the 7th Int. Conference on Verification, Model Checking, and Abstract Interpretation, 2006.","DOI":"10.1007\/11609773_11"},{"key":"10.1016\/j.jcss.2011.08.003_br0310","doi-asserted-by":"crossref","unstructured":"Greta Yorsh, Alexander M. Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani, A logic of reachable patterns in linked data-structures, in: FoSSaCS, 2006, pp. 94\u2013110.","DOI":"10.1007\/11690634_7"}],"container-title":["Journal of Computer and System Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000011000821?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000011000821?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,3,8]],"date-time":"2025-03-08T20:31:44Z","timestamp":1741465904000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0022000011000821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,5]]}},"alternative-id":["S0022000011000821"],"URL":"https:\/\/doi.org\/10.1016\/j.jcss.2011.08.003","relation":{},"ISSN":["0022-0000"],"issn-type":[{"type":"print","value":"0022-0000"}],"subject":[],"published":{"date-parts":[[2012,5]]}}}