{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:13Z","timestamp":1725514873776},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_8","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"84-99","source":"Crossref","is-referenced-by-count":4,"title":["Verifying Dynamic Pointer-Manipulating Threads"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Noll","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Rieger","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape Analysis by Predicate Abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 532\u2013546. Springer, Heidelberg (2006)"},{"key":"8_CR3","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_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11823230_5","volume-title":"Static Analysis","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 52\u201370. Springer, Heidelberg (2006)"},{"key":"8_CR6","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_CR7","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1145\/93542.93585","volume-title":"PLDI 1990","author":"D.R. Chase","year":"1990","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: PLDI 1990, pp. 296\u2013310. ACM Press, New York (1990)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-36384-X_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2002","unstructured":"Dams, D., Namjoshi, K.S.: Shape Analysis through Predicate Abstraction and Model Checking. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 310\u2013323. Springer, Heidelberg (2002)"},{"key":"8_CR9","first-page":"51","volume-title":"LICS 2001","author":"S. Das","year":"2001","unstructured":"Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: LICS 2001, pp. 51\u201358. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/11804192_14","volume-title":"Formal Methods for Components and Objects","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Safety and liveness in concurrent pointer programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 280\u2013312. Springer, Heidelberg (2006)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BFb0017477","volume-title":"Trees in Algebra and Programming - CAAP \u201994","author":"J. Esparza","year":"1994","unstructured":"Esparza, J.: On the decidability of model checking for several \u03bc-calculi and Petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 115\u2013129. Springer, Heidelberg (1994)"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1145\/1250734.1250765","volume-title":"PLDI 2007","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI 2007, pp. 266\u2013277. ACM Press, New York (2007)"},{"unstructured":"Havelund, K., Rosu, G.: Testing linear temporal logic formulae on finite execution traces. Technical Report TR\u00a001-08, RIACS (2001)","key":"8_CR14"},{"unstructured":"Katoen, J.-P., Noll, T., Rieger, S.: Verifying concurrent list-manipulating programs by LTL model checking. Technical Report 2007-06, RWTH Aachen University, Dept. of Computer Science, Germany (April 2007)","key":"8_CR15"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1145\/1111037.1111048","volume-title":"POPL 2006","author":"S.K. Lahiri","year":"2006","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL 2006, pp. 115\u2013126. ACM Press, New York (2006)"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(92)90173-D","volume":"99","author":"J.L. Lambert","year":"1992","unstructured":"Lambert, J.L.: A structure to decide reachability in Petri nets. Theor. Comput. Sci.\u00a099(1), 79\u2013104 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/11532231_8","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Lev-Ami","year":"2005","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, S., Srivastava, S., Yorsh, G.: Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 99\u2013115. Springer, Heidelberg (2005)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-71209-1_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Manevich","year":"2007","unstructured":"Manevich, R., Berdine, J., Cook, B., Ramalingam, G., Sagiv, M.: Shape analysis by graph decomposition. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 3\u201318. Springer, Heidelberg (2007)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-3-540-27864-1_14","volume-title":"Static Analysis","author":"E.M. Nystrom","year":"2004","unstructured":"Nystrom, E.M., Kim, H.-S., Hwu, W.W.: Bottom-up and top-down context-sensitive summary-based pointer analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 165\u2013180. Springer, Heidelberg (2004)"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/964001.964024","volume-title":"POPL 2004","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268\u2013280. ACM Press, New York (2004)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11547662_19","volume-title":"Static Analysis","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean Heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 268\u2013283. Springer, Heidelberg (2005)"},{"key":"8_CR24","first-page":"55","volume-title":"LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"issue":"5","key":"8_CR25","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/301631.301645","volume":"34","author":"R. Rugina","year":"1999","unstructured":"Rugina, R., Rinard, M.: Pointer analysis for multithreaded programs. SIGPLAN Not.\u00a034(5), 77\u201390 (1999)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"8_CR26","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 Trans. Program. Lang. Syst.\u00a020(1), 1\u201350 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"8_CR27","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/379539.379553","volume-title":"PPoPP 2001","author":"A. Salcianu","year":"2001","unstructured":"Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: PPoPP 2001, pp. 12\u201323. ACM Press, New York (2001)"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/1133981.1134022","volume-title":"PLDI 2006","author":"M.T. Vechev","year":"2006","unstructured":"Vechev, M.T., Yahav, E., Bacon, D.F.: Correctness-preserving derivation of concurrent garbage collection algorithms. In: PLDI 2006, pp. 341\u2013353. ACM Press, New York (2006)"},{"issue":"3","key":"8_CR30","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/373243.360206","volume":"36","author":"E. Yahav","year":"2001","unstructured":"Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. ACM SIGPLAN Notices\u00a036(3), 27\u201340 (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR31","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)"},{"issue":"1","key":"8_CR32","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0890-5401(92)90059-O","volume":"96","author":"H.-C. Yen","year":"1992","unstructured":"Yen, H.-C.: A unified approach for deciding the existence of certain Petri net paths. Inf. Comput.\u00a096(1), 119\u2013137 (1992)","journal-title":"Inf. Comput."},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-540-27864-1_12","volume-title":"Static Analysis","author":"S.H. Yong","year":"2004","unstructured":"Yong, S.H., Horwitz, S.: Pointer-range analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 133\u2013148. Springer, Heidelberg (2004)"},{"key":"8_CR34","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/996841.996860","volume-title":"PLDI 2004","author":"J. Zhu","year":"2004","unstructured":"Zhu, J., Calman, S.: Symbolic pointer analysis revisited. In: PLDI 2004, pp. 145\u2013157. ACM Press, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:43:48Z","timestamp":1620017028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_8","relation":{},"subject":[]}}