{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:33Z","timestamp":1725487233360},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727323"},{"type":"electronic","value":"9783540727347"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72734-7_8","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T09:40:50Z","timestamp":1183023650000},"page":"100-114","source":"Crossref","is-referenced-by-count":6,"title":["Reasoning About Sequences of Memory States"],"prefix":"10.1007","author":[{"given":"R\u00e9mi","family":"Brochenin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Etienne","family":"Lozes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. JACM\u00a041, 181\u2013204 (1994)","journal-title":"JACM"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1016\/B978-044482830-9\/50027-8","volume-title":"Handbook of Process Algebra","author":"O. Burkart","year":"2001","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification of infinite structures. In: Handbook of Process Algebra, pp. 545\u2013623. Elsevier, Amsterdam (2001)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"8_CR5","unstructured":"Brochenin, R., Demri, S., Lozes, E.: Reasoning about sequences of memory states. Technical report, LSV, ENS de Cachan (2007)"},{"key":"8_CR6","unstructured":"Bardin, S., Finkel, A., Lozes, E., Sangnier, A.: From pointer systems to counter systems using shape analysis. In: 5th International Workshop on Automated Verification of Infinite-State Systems, AVIS\u201906 (2006)"},{"key":"8_CR7","unstructured":"Bardin, S., Finkel, A., Nowak, D.: Toward symbolic verification of programs handling pointers. In: 3rd International Workshop on Automated Verification of Infinite-State Systems, AVIS\u201904 (2004)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/978-3-540-27864-1_25","volume-title":"Static Analysis","author":"M. Bozga","year":"2004","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: On logics of aliasing. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 344\u2013360. Springer, Heidelberg (2004)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-44622-2_17","volume-title":"Computer Science Logic","author":"H. Comon","year":"2000","unstructured":"Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 262\u2013276. Springer, Heidelberg (2000)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/978-3-540-31982-5_25","volume-title":"Foundations of Software Science and Computational Structures","author":"C. Calcagno","year":"2005","unstructured":"Calcagno, C., Gardner, P., Hague, M.: From separation logic to first-order logic. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 395\u2013409. Springer, Heidelberg (2005)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C. Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a02245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S. Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Information and Computation\u00a0205(3), 380\u2013415 (2007)","journal-title":"Information and Computation"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/978-3-540-30538-5_21","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"D. Distefano","year":"2004","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Who is pointing when to whom? On the automated verification of linked list structures. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 250\u2013262. Springer, Heidelberg (2004)"},{"key":"8_CR14","volume-title":"Many-dimensional modal logics: theory and applications","author":"D. Gabbay","year":"2003","unstructured":"Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics: theory and applications. CUP, Cambridge (2003)"},{"key":"8_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11591191_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Galmiche","year":"2005","unstructured":"Galmiche, D., Mery, D.: Characterizing provability in BI\u2019s pointer logic through resource graphs. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 459\u2013473. Springer, Heidelberg (2005)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: POPL\u201901, pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1145\/258915.258936","volume-title":"PLDI\u201997","author":"J. Jensen","year":"1997","unstructured":"Jensen, J., Jorgensen, M., Klarlund, N., Schwartzbach, M.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI\u201997, pp. 226\u2013236. ACM Press, New York (1997)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013302. Springer, Heidelberg (2000)"},{"key":"8_CR19","unstructured":"Lozes, E.: Separation logic preserves the expressive power of classical logic. In: 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, SPACE\u201904 (2004)"},{"key":"8_CR20","first-page":"46","volume-title":"FOCS\u201977","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS\u201977, pp. 46\u201357. IEEE Computer Society Press, Los Alamitos (1977)"},{"key":"8_CR21","first-page":"55","volume-title":"LICS\u201902","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS\u201902, pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"issue":"3","key":"8_CR22","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logic. JACM\u00a032(3), 733\u2013749 (1985)","journal-title":"JACM"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115, 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-36575-3_15","volume-title":"Programming Languages and Systems","author":"E. Yahav","year":"2003","unstructured":"Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72734-7_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:04:53Z","timestamp":1605762293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72734-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727323","9783540727347"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72734-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}