{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:07Z","timestamp":1725494287433},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540755951"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75596-8_12","type":"book-chapter","created":{"date-parts":[[2007,11,3]],"date-time":"2007-11-03T14:03:37Z","timestamp":1194098617000},"page":"145-161","source":"Crossref","is-referenced-by-count":6,"title":["Proving Termination of Tree Manipulating Programs"],"prefix":"10.1007","author":[{"given":"Peter","family":"Habermehl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"VMCAI 2005","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, Springer, Heidelberg (2005)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45420-9","volume-title":"CAV 2001","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"12_CR3","volume-title":"Proc. of POPL 2007","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.: Analyses from Invariance Analyses. In: Proc. of POPL 2007, ACM Press, New York (2007)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 2006","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, Springer, Heidelberg (2006)"},{"key":"12_CR5","first-page":"37","volume":"149","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking. ENTCS\u00a0149, 37\u201348 (2006)","journal-title":"ENTCS"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"SAS 2006","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, Springer, Heidelberg (2006)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"ICALP 2006","author":"M. Bozga","year":"2006","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat Parametric Counter Automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, Springer, Heidelberg (2006)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"ICALP 2005","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The Polyranking Principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, Springer, Heidelberg (2005)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient Verification of Sequential and Concurrent C Programs. Formal Methods in System Design\u00a025(2\u20133) (2004)","DOI":"10.1023\/B:FORM.0000040026.56959.91"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 2000","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027094","volume-title":"CAV 1998","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"SAS 2005","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction Refinement for Termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, Springer, Heidelberg (2005)"},{"key":"12_CR13","volume-title":"Proc. of PLDI 2006","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination Proofs for Systems Code. In: Proc. of PLDI 2006, ACM Press, New York (2006)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 2006","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"12_CR15","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"TACAS 2006","author":"J.V. Deshmukh","year":"2006","unstructured":"Deshmukh, J.V., Emerson, E.A., Gupta, P.: Automatic Verification of Parameterized Data Structures. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, Springer, Heidelberg (2006)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 2006","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., Berdine, J., Cook, B., O\u2019Hearn, P.W.: Automatic Termination Proofs for Programs with Shape-shifting Heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"12_CR18","unstructured":"Habermehl, P., Iosif, R., Rogalewicz, A., Vojnar, T.: Proving Termination of Tree Manipulating Programs. Verimag, TR-2007 -1, http:\/\/www-verimag.imag.fr\/index.php?page=techrep-list"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b94220","volume-title":"SPIN 2003","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, Springer, Heidelberg (2003)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"SAS 2006","author":"A. Loginov","year":"2006","unstructured":"Loginov, A., Reps, T.W., Sagiv, M.: Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, Springer, Heidelberg (2006)"},{"key":"12_CR21","volume-title":"Proc. of PLDI 2001","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. of PLDI 2001, ACM Press, New York (2001)"},{"key":"12_CR22","volume-title":"Proc. of LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proc. of LICS 2002, IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"12_CR23","unstructured":"Rybalchenko, A.: The ARMC tool, http:\/\/www.mpi-inf.mpg.de\/~rybal\/armc\/"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric Shape Analysis via 3-valued Logic. TOPLAS\u00a024(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"ESOP 2003","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, Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75596-8_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:25:21Z","timestamp":1619519121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75596-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755951"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75596-8_12","relation":{},"subject":[]}}