{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:14:26Z","timestamp":1740028466558,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540240587"},{"type":"electronic","value":"9783540305385"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30538-5_21","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:40:30Z","timestamp":1268401230000},"page":"250-262","source":"Crossref","is-referenced-by-count":14,"title":["Who is Pointing When to Whom?"],"prefix":"10.1007","author":[{"given":"Dino","family":"Distefano","sequence":"first","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Arend","family":"Rensink","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Bardin, S., Finkel, A., Nowak, D.: Towards symbolic verification of programs handling pointers. In: AVIS 2004. ENTCS (2004)(to appear)"},{"key":"21_CR2","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1145\/777388.777395","volume-title":"PEPM","author":"M. Bozga","year":"2003","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Storeless semantics and alias logic. In: PEPM, pp. 55\u201365. ACM Press, New York (2003)"},{"key":"21_CR3","first-page":"23","volume":"6","author":"R. Burstall","year":"1971","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence\u00a06, 23\u201350 (1971)","journal-title":"Machine Intelligence"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/3-540-45465-9_51","volume-title":"Automata, Languages and Programming","author":"L. Cardelli","year":"2002","unstructured":"Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 597\u2013610. Springer, Heidelberg (2002)"},{"key":"21_CR5","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/325694.325742","volume-title":"POPL","author":"L. Cardelli","year":"2000","unstructured":"Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: POPL, pp. 365\u2013377. ACM Press, New York (2000)"},{"key":"21_CR6","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1145\/93542.93585","volume-title":"PLDI","author":"D.R. Chase","year":"1990","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: PLDI, pp. 296\u2013310. ACM Press, New York (1990)"},{"key":"21_CR7","first-page":"160","volume-title":"POPL","author":"S.A. Cook","year":"1975","unstructured":"Cook, S.A., Oppen, D.: An assertion language for data structures. In: POPL, pp. 160\u2013166. ACM Press, New York (1975)"},{"key":"21_CR8","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1145\/178243.178263","volume-title":"PLDI","author":"A. Deutsch","year":"1994","unstructured":"Deutsch, A.: Interprocedural may-alias analysis for pointers: beyond k-limiting. In: PLDI, pp. 230\u2013241. ACM Press, New York (1994)"},{"key":"21_CR9","unstructured":"Distefano, D.: On model checking the dynamics of object-based software: a foundational approach. PhD. Thesis, Univ. of Twente (2003)"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Distefano, D., Rensink, A., Katoen, J.-P.: Who is pointing when to whom? CTIT Tech. Rep. 03-12 (2003)","DOI":"10.1007\/978-3-540-30538-5_21"},{"key":"21_CR11","first-page":"435","volume-title":"TCS","author":"D. Distefano","year":"2002","unstructured":"Distefano, D., Rensink, A., Katoen, J.-P.: Model checking birth and death. In: TCS, pp. 435\u2013447. Kluwer, Dordrecht (2002)"},{"key":"21_CR12","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/360204.375719","volume-title":"POPL","author":"S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14\u201326. ACM Press, New York (2001)"},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1145\/258915.258936","volume-title":"PLDI","author":"J. Jensen","year":"1997","unstructured":"Jensen, J., J\u00f8rgensen, M., Schwartzbach, M., Klarlund, N.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI, pp. 226\u2013236. ACM Press, New York (1997)"},{"key":"21_CR14","first-page":"102","volume-title":"Program Flow Analysis: Theory and Applications, ch. 4","author":"N.D. Jones","year":"1981","unstructured":"Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of Lisp-like structures. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, ch. 4, pp. 102\u2013131. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"21_CR15","first-page":"97","volume-title":"POPL","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97\u2013107. ACM Press, New York (1985)"},{"key":"21_CR16","first-page":"38","volume-title":"POPL","author":"G. Nelson","year":"1983","unstructured":"Nelson, G.: Verifying reachability invariants of linked structures. In: POPL, pp. 38\u201347. ACM Press, New York (1983)"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Montanari, U., Pistore, M.: An introduction to history-dependent automata. ENTCS\u00a010 (1998)","DOI":"10.1016\/S1571-0661(05)80696-6"},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/964001.964024","volume-title":"POPL","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL, pp. 268\u2013280. ACM Press, New York (2004)"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-24725-8_28","volume-title":"Programming Languages and Systems","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 401\u2013415. Springer, Heidelberg (2004)"},{"key":"21_CR20","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE CS Press, Los Alamitos (2002)"},{"issue":"1","key":"21_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS\u00a020(1), 1\u201350 (1998)","journal-title":"ACM TOPLAS"},{"key":"21_CR22","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/343647.343788","volume-title":"DATE","author":"L. S\u00e9m\u00e9ria","year":"2000","unstructured":"S\u00e9m\u00e9ria, L., Sato, K., de Micheli, G.: Resolution of dynamic memory allocation and pointers for the behavioural synthesis from C. In: DATE, pp. 312\u2013319. ACM Press, New York (2000)"},{"key":"21_CR23","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. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30538-5_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T12:11:29Z","timestamp":1739967089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30538-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540240587","9783540305385"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30538-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}