{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:27Z","timestamp":1725471147469},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540367499"},{"type":"electronic","value":"9783540367505"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11804192_14","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T04:20:46Z","timestamp":1159503646000},"page":"280-312","source":"Crossref","is-referenced-by-count":5,"title":["Safety and Liveness in Concurrent Pointer Programs"],"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":[{"unstructured":"Bardin, S., Finkel, A., Nowak, D.: Towards symbolic verification of programs handling pointers. In: AVIS 2004 (2004)","key":"14_CR1"},{"key":"14_CR2","volume-title":"Find the Bug in this Java Program","author":"A. Barr","year":"2005","unstructured":"Barr, A.: Find the Bug in this Java Program. Addison-Wesley, Reading (2005)"},{"issue":"3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1008278803780","volume":"7","author":"D. Basin","year":"1998","unstructured":"Basin, D., Matthews, S., Vigano, L.: Labelled modal logics: quantifiers. J. of Logic, Language and Information\u00a07(3), 237\u2013263 (1998)","journal-title":"J. of Logic, Language and Information"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"14_CR5","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)"},{"volume-title":"Handbook of Process Algebra","year":"2001","unstructured":"Bergstra, J., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)","key":"14_CR6"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-540-31980-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked list structures in regular model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 13\u201329. Springer, Heidelberg (2005)"},{"key":"14_CR8","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":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"14_CR10","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":"14_CR11","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":"14_CR12","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":"14_CR13","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":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-44898-5_26","volume-title":"Static Analysis","author":"S. Chong","year":"2003","unstructured":"Chong, S., Rugina, R.: Static analysis of accessed regions in recursive data structures. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 463\u2013482. Springer, Heidelberg (2003)"},{"key":"14_CR15","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":"14_CR16","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":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11575467_26","volume-title":"Programming Languages and Systems","author":"D. Distefano","year":"2005","unstructured":"Distefano, D.: A parametric model for the analysis of mobile ambients. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 401\u2013417. Springer, Heidelberg (2005)"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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? \u2013 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)"},{"unstructured":"Distefano, D., Rensink, A., Katoen, J.-P.: Who is pointing when to whom? \u2013 On the automated verification of linked list structures CTIT Tech. Rep. 03-12 (2003)","key":"14_CR19"},{"key":"14_CR20","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)"},{"issue":"1","key":"14_CR21","first-page":"5","volume":"39","author":"M. Fitting","year":"1999","unstructured":"Fitting, M.: On quantified modal logic. Fundamenta Informatica\u00a039(1), 5\u2013121 (1999)","journal-title":"Fundamenta Informatica"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/3-540-61055-3_33","volume-title":"Programming Languages and Systems - ESOP 1996","author":"P. Fradet","year":"1996","unstructured":"Fradet, P., Gaugne, R., Le M\u00e9tayer, D.: Static detection of pointer errors: an axiomatisation and a checking algorithm. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol.\u00a01058, pp. 125\u2013140. Springer, Heidelberg (1996)"},{"unstructured":"van Glabbeek, R.J.: The linear time-branching time spectrum I. In: [6], ch. 1, pp. 3\u2013101 (2001)","key":"14_CR23"},{"key":"14_CR24","first-page":"14","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":"14_CR25","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":"14_CR26","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, ch. 4. 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":"14_CR27","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":"14_CR28","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":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-30579-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 181\u2013198. Springer, Heidelberg (2005)"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"A Calculus of Communication Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"doi-asserted-by":"crossref","unstructured":"Montanari, U., Pistore, M.: An introduction to history-dependent automata. ENTCS\u00a010 (1998)","key":"14_CR31","DOI":"10.1016\/S1571-0661(05)80696-6"},{"key":"14_CR32","first-page":"213","volume-title":"PLDI","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.: The pointer assertion logic engine. In: PLDI, pp. 213\u2013221. ACM Press, New York (2001)"},{"unstructured":"Morris, J.: Assignment and linked data structures. In: Th. Found. of Progr. Meth., Reidel, pp. 25\u201334 (1981)","key":"14_CR33"},{"key":"14_CR34","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":"14_CR35","first-page":"46","volume-title":"FOCS","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE CS Press, Los Alamitos (1977)"},{"key":"14_CR36","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":"14_CR37","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":"14_CR38","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":"14_CR39","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":"14_CR40","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)"},{"key":"14_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-45789-5_8","volume-title":"Static Analysis","author":"T. Yavuz-Kahveci","year":"2002","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 69\u201382. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11804192_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T20:45:41Z","timestamp":1683578741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11804192_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540367499","9783540367505"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/11804192_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}