{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T10:15:11Z","timestamp":1676974511673},"reference-count":36,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2009,12,1]],"date-time":"2009-12-01T00:00:00Z","timestamp":1259625600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,12,1]],"date-time":"2013-12-01T00:00:00Z","timestamp":1385856000000},"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":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1016\/j.apal.2009.07.004","type":"journal-article","created":{"date-parts":[[2009,8,26]],"date-time":"2009-08-26T10:13:53Z","timestamp":1251281633000},"page":"305-323","source":"Crossref","is-referenced-by-count":10,"title":["Reasoning about sequences of memory states"],"prefix":"10.1016","volume":"161","author":[{"given":"R\u00e9mi","family":"Brochenin","sequence":"first","affiliation":[]},{"given":"St\u00e9phane","family":"Demri","sequence":"additional","affiliation":[]},{"given":"Etienne","family":"Lozes","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.apal.2009.07.004_b1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","article-title":"A really temporal logic","volume":"41","author":"Alur","year":"1994","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/j.apal.2009.07.004_b2","series-title":"FROCOS\u201902","first-page":"162","article-title":"Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning","volume":"vol. 2309","author":"Balbiani","year":"2002"},{"key":"10.1016\/j.apal.2009.07.004_b3","series-title":"FOSSACS\u201909","first-page":"425","article-title":"Beyond shapes: Lists with ordered data","volume":"vol. 5504","author":"Bansal","year":"2009"},{"key":"10.1016\/j.apal.2009.07.004_b4","unstructured":"S. Bardin, A. Finkel, E. Lozes, A. Sangnier, From pointer systems to counter systems using shape analysis, in: 5th International Workshop on Automated Verification of Infinite-State Systems (AVIS\u201906)"},{"key":"10.1016\/j.apal.2009.07.004_b5","unstructured":"S. Bardin, A. Finkel, D. Nowak, Toward symbolic verification of programs handling pointers, in: 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS\u201904), 2004"},{"issue":"3","key":"10.1016\/j.apal.2009.07.004_b6","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1023\/A:1020083231504","article-title":"Multi-dimensional modal logic as a framework for spatio-temporal reasoning","volume":"17","author":"Bennett","year":"2002","journal-title":"Applied Intelligence"},{"key":"10.1016\/j.apal.2009.07.004_b7","series-title":"CAV","first-page":"178","article-title":"Shape analysis for composite data structures","volume":"vol. 4590","author":"Berdine","year":"2007"},{"key":"10.1016\/j.apal.2009.07.004_b8","series-title":"APLAS\u201905","first-page":"52","article-title":"Symbolic execution with separation logic","volume":"vol. 3780","author":"Berdine","year":"2005"},{"key":"10.1016\/j.apal.2009.07.004_b9","series-title":"FMCO\u201905","first-page":"115","article-title":"Smallfoot: Modular automatic assertion checking with separation logic","volume":"vol. 4111","author":"Berdine","year":"2005"},{"key":"10.1016\/j.apal.2009.07.004_b10","series-title":"CAV\u201906","first-page":"517","article-title":"Programs with lists are counter automata","volume":"vol. 4144","author":"Bouajjani","year":"2006"},{"key":"10.1016\/j.apal.2009.07.004_b11","unstructured":"A. Bouajjani, R. Echahed, P. Habermehl, On the verification problem of nonregular properties for nonregular processes, in: LICS\u201995, 1995, pp. 123\u2013133"},{"key":"10.1016\/j.apal.2009.07.004_b12","series-title":"SAS\u201904","first-page":"344","article-title":"On logics of aliasing","volume":"vol. 3148","author":"Bozga","year":"2004"},{"key":"10.1016\/j.apal.2009.07.004_b13","series-title":"LFCS\u201907","first-page":"100","article-title":"Reasoning about sequences of memory states","volume":"vol. 4514","author":"Brochenin","year":"2007"},{"key":"10.1016\/j.apal.2009.07.004_b14","series-title":"CSL\u201908","first-page":"322","article-title":"On the almighty wand","volume":"vol. 5213","author":"Brochenin","year":"2008"},{"key":"10.1016\/j.apal.2009.07.004_b15","series-title":"Handbook of Process Algebra","first-page":"545","article-title":"Verification of infinite structures","author":"Burkart","year":"2001"},{"key":"10.1016\/j.apal.2009.07.004_b16","series-title":"FOSSACS\u201905","first-page":"395","article-title":"From separation logic to first-order logic","volume":"vol. 3441","author":"Calcagno","year":"2005"},{"key":"10.1016\/j.apal.2009.07.004_b17","series-title":"FST&TCS\u201901","first-page":"108","article-title":"Computability and complexity results for a spatial assertion language for data structures","volume":"vol. 2245","author":"Calcagno","year":"2001"},{"key":"10.1016\/j.apal.2009.07.004_b18","series-title":"CSL\u201900","first-page":"262","article-title":"Flatness is not a weakness","volume":"vol. 1862","author":"Comon","year":"2000"},{"issue":"3","key":"10.1016\/j.apal.2009.07.004_b19","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","article-title":"An automata-theoretic approach to constraint LTL","volume":"205","author":"Demri","year":"2007","journal-title":"Information and Computation"},{"key":"10.1016\/j.apal.2009.07.004_b20","doi-asserted-by":"crossref","unstructured":"S. Demri, R. Gascon, The effects of bounding syntactic resources on Presburger LTL, Journal of Logic and Computation (in press)","DOI":"10.1109\/TIME.2007.63"},{"key":"10.1016\/j.apal.2009.07.004_b21","series-title":"FST&TCS\u201904","first-page":"250","article-title":"Who is pointing when to whom? on the automated verification of linked list structures","volume":"vol. 3328","author":"Distefano","year":"2004"},{"key":"10.1016\/j.apal.2009.07.004_b22","unstructured":"A. Finkel, E. Lozes, A. Sangnier, Towards model-checking programs with lists, in: Infinity in Logic and Computation, vol. 5489, in: Lecture Notes in Artificial Intelligence, Springer, 2009 (in press)"},{"key":"10.1016\/j.apal.2009.07.004_b23","series-title":"Many-Dimensional Modal Logics: Theory and Applications","author":"Gabbay","year":"2003"},{"key":"10.1016\/j.apal.2009.07.004_b24","series-title":"7th Annual ACM Symposium on Principles of Programming Languages","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980"},{"key":"10.1016\/j.apal.2009.07.004_b25","series-title":"LPAR\u201905","first-page":"459","article-title":"Characterizing provability in BI\u2019s pointer logic through resource graphs","volume":"vol. 3835","author":"Galmiche","year":"2005"},{"key":"10.1016\/j.apal.2009.07.004_b26","doi-asserted-by":"crossref","unstructured":"D. Galmiche, D. M\u00e9ry, Tableaux and resource graphs for separation logic, Journal of Logic and Computation (in press)","DOI":"10.1093\/logcom\/exn066"},{"key":"10.1016\/j.apal.2009.07.004_b27","doi-asserted-by":"crossref","unstructured":"S. Ishtiaq, P. O\u2019Hearn, BI as an assertion language for mutable data structures, in: POPL\u201901, 2001, pp. 14\u201326","DOI":"10.1145\/373243.375719"},{"key":"10.1016\/j.apal.2009.07.004_b28","series-title":"PLDI\u201997","first-page":"226","article-title":"Automatic verification of pointer programs using monadic second-order logic","author":"Jensen","year":"1997"},{"issue":"2","key":"10.1016\/j.apal.2009.07.004_b29","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","article-title":"An automata-theoretic approach to branching-time model checking","volume":"47","author":"Kupferman","year":"2000","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/j.apal.2009.07.004_b30","doi-asserted-by":"crossref","unstructured":"T. Lev-Ami, M. Sagiv, TVLA: A system for implementing static analyses, in: SAS\u201900, 2000, pp. 280\u2013301","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"10.1016\/j.apal.2009.07.004_b31","unstructured":"E. Lozes, Expressivit\u00e9 des logiques spatiales, Ph.D. Thesis, Laboratoire de l\u2019Informatique du Parall\u00e9lisme, ENS Lyon, France, 2004"},{"key":"10.1016\/j.apal.2009.07.004_b32","series-title":"FOCS\u201977","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/j.apal.2009.07.004_b33","series-title":"LICS\u201902","first-page":"55","article-title":"Separation logic: a logic for shared mutable data structures","author":"Reynolds","year":"2002"},{"issue":"3","key":"10.1016\/j.apal.2009.07.004_b34","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logic","volume":"32","author":"Sistla","year":"1985","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/j.apal.2009.07.004_b35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computations","volume":"115","author":"Vardi","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/j.apal.2009.07.004_b36","series-title":"ESOP\u201903","first-page":"204","article-title":"Verifying temporal heap properties specified via evolution logic","volume":"vol. 2618","author":"Yahav","year":"2003"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007209001444?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007209001444?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T05:20:39Z","timestamp":1558502439000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007209001444"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["S0168007209001444"],"URL":"https:\/\/doi.org\/10.1016\/j.apal.2009.07.004","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2009,12]]}}}