{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:19:19Z","timestamp":1743027559477,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221095"},{"type":"electronic","value":"9783642221101"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_34","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"424-440","source":"Crossref","is-referenced-by-count":19,"title":["Forest Automata for Verification of Heap Manipulation"],"prefix":"10.1007","author":[{"given":"Peter","family":"Habermehl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"\u0160im\u00e1\u010dek","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":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-70545-1_33","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2008","unstructured":"Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Rezine, A.: Monotonic Abstraction for Programs with Dynamic Memory Heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 341\u2013354. Springer, Heidelberg (2008)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-78800-3_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2008","unstructured":"Abdulla, P.A., Bouajjani, A., Hol\u00edk, L., Kaati, L., Vojnar, T.: Computing Simulations over Tree Automata. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 93\u2013108. Springer, Heidelberg (2008)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When Simulation Meets Antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 158\u2013174. Springer, Heidelberg (2010)"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape Analysis for Composite Data Structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"34_CR5","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":"34_CR6","volume-title":"ENTCS","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking. In: ENTCS, vol.\u00a0149(1), Elsevier, Amsterdam (2006)"},{"key":"34_CR7","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":"34_CR8","volume-title":"Proc. of POPL 2009","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional Shape Analysis by Means of Bi-abduction. In: Proc. of POPL 2009. ACM Press, New York (2009)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/11691372_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.V. Deshmukh","year":"2006","unstructured":"Deshmukh, J.V., Emerson, E.A., Gupta, P.: Automatic Verification of Parameterized Data Structures. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 27\u201341. Springer, Heidelberg (2006)"},{"key":"34_CR10","volume-title":"Proc. of PLDI 2007","author":"B. Guo","year":"2007","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape Analysis with Inductive Recursion Synthesis. In: Proc. of PLDI 2007. ACM Press, New York (2007)"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Hol\u00edk, L., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forest Automata for Verification of Heap Manipulation. Technical Report FIT-TR-2011-01, FIT BUT, Czech Republic (2011), \n                  \n                    http:\/\/www.fit.vutbr.cz\/~isimacek\/pub\/FIT-TR-2011-01.pdf","DOI":"10.1007\/978-3-642-22110-1_34"},{"key":"34_CR12","volume-title":"Proc. of POPL 2011","author":"P. Madhusudan","year":"2011","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable Logics Combining Heap Structures and Data. In: Proc. of POPL 2011. ACM Press, New York (2011)"},{"key":"34_CR13","volume-title":"Proc. of PLDI 2001","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.: The Pointer Assertion Logic Engine. In: Proc. of PLDI 2001. ACM Press, New York (2001)"},{"key":"34_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated Verification of Shape and Size Properties Via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"34_CR15","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":"34_CR16","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":"34_CR17","unstructured":"Yang, H., Lee, O., Calcagno, C., Distefano, D., O\u2019Hearn, P.W.: On Scalable Shape Analysis. Technical report RR-07-10, Queen Mary, University of London (2007)"},{"key":"34_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable Shape Analysis for Systems Code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"},{"key":"34_CR19","volume-title":"Proc. of PLDI 2008","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full Functional Verification of Linked Data Structures. In: Proc. of PLDI 2008. ACM Press, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:06:53Z","timestamp":1558296413000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}