{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:28:09Z","timestamp":1774837689825,"version":"3.50.1"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,4,11]],"date-time":"2012-04-11T00:00:00Z","timestamp":1334102400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10703-012-0150-8","type":"journal-article","created":{"date-parts":[[2012,4,10]],"date-time":"2012-04-10T12:59:58Z","timestamp":1334062798000},"page":"83-106","source":"Crossref","is-referenced-by-count":18,"title":["Forest automata for verification of heap manipulation"],"prefix":"10.1007","volume":"41","author":[{"given":"Peter","family":"Habermehl","sequence":"first","affiliation":[]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"\u0160im\u00e1\u010dek","sequence":"additional","affiliation":[]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,4,11]]},"reference":[{"key":"150_CR1","series-title":"LNCS","volume-title":"Proc of CAV\u201908","author":"PA Abdulla","year":"2008","unstructured":"Abdulla PA, Bouajjani A, Cederberg J, Haziza F, Rezine A (2008) Monotonic abstraction for programs with dynamic memory heaps. In: Proc of CAV\u201908. LNCS, vol 5123. Springer, Berlin"},{"key":"150_CR2","series-title":"LNCS","volume-title":"Proc of TACAS\u201908","author":"PA Abdulla","year":"2008","unstructured":"Abdulla PA, Bouajjani A, Hol\u00edk L, Kaati L, Vojnar T (2008) Computing simulations over tree automata: efficient techniques for reducing TA. In: Proc of TACAS\u201908. LNCS, vol\u00a04963"},{"key":"150_CR3","series-title":"LNCS","volume-title":"Proc of TACAS\u201910","author":"PA Abdulla","year":"2010","unstructured":"Abdulla PA, Chen Y-F, Hol\u00edk L, Mayr R, Vojnar T (2010) When simulation meets antichains (on checking language inclusion of NFAs). In: Proc of TACAS\u201910. LNCS, vol 6015. Springer, Berlin"},{"key":"150_CR4","series-title":"LNCS","volume-title":"Proc CAV\u201907","author":"J Berdine","year":"2007","unstructured":"Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW, Wies T, Yang H (2007) Shape analysis for composite data structures. In: Proc CAV\u201907. LNCS, vol 4590. Springer, Berlin"},{"key":"150_CR5","series-title":"LNCS","volume-title":"Proc of CAV\u201906","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani A, Bozga M, Habermehl P, Iosif R, Moro P, Vojnar T (2006) Programs with lists are counter automata. In: Proc of CAV\u201906. LNCS, vol 4144. Springer, Berlin"},{"issue":"1","key":"150_CR6","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.entcs.2005.11.015","volume":"149","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani A, Habermehl P, Rogalewicz A, Vojnar T (2006) Abstract regular tree model checking. Electron Notes Theor Comput Sci 149(1):37\u201348","journal-title":"Electron Notes Theor Comput Sci"},{"key":"150_CR7","series-title":"LNCS","volume-title":"Proc of SAS\u201906","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani A, Habermehl P, Rogalewicz A, Vojnar T (2006) Abstract regular tree model checking of complex dynamic data structures. In: Proc of SAS\u201906. LNCS, vol 4134. Springer, Berlin"},{"key":"150_CR8","volume-title":"Proc of POPL\u201909","author":"C Calcagno","year":"2009","unstructured":"Calcagno C, Distefano D, O\u2019Hearn PW, Yang H (2009) Compositional shape analysis by means of Bi-abduction. In: Proc of POPL\u201909. ACM, New York"},{"key":"150_CR9","series-title":"LNCS","volume-title":"Proc of TACAS\u201906","author":"JV Deshmukh","year":"2006","unstructured":"Deshmukh JV, Emerson EA, Gupta P (2006) Automatic verification of parameterized data structures. In: Proc of TACAS\u201906. LNCS, vol 3920. Springer, Berlin"},{"key":"150_CR10","series-title":"LNCS","volume-title":"Proc of CAV\u201911","author":"K Dudka","year":"2011","unstructured":"Dudka K, Peringer P, Vojnar T (2011) Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Proc of CAV\u201911. LNCS, vol 6806. Springer, Berlin"},{"key":"150_CR11","volume-title":"Proc of PLDI\u201907","author":"B Guo","year":"2007","unstructured":"Guo B, Vachharajani N, August DI (2007) Shape analysis with inductive recursion synthesis. In: Proc of PLDI\u201907. ACM, New York"},{"key":"150_CR12","doi-asserted-by":"crossref","unstructured":"Habermehl P, Hol\u00edk L, Rogalewicz A, \u0160im\u00e1\u010dek J, Vojnar T (2011) Forest automata for verification of heap manipulation. Technical report FIT-TR-2011-01, FIT BUT, Czech Republic. http:\/\/www.fit.vutbr.cz\/~isimacek\/pub\/FIT-TR-2011-01.pdf","DOI":"10.1007\/978-3-642-22110-1_34"},{"key":"150_CR13","volume-title":"Proc of POPL\u201911","author":"P Madhusudan","year":"2011","unstructured":"Madhusudan P, Parlato G, Qiu X (2011) Decidable logics combining heap structures and data. In: Proc of POPL\u201911. ACM, New York"},{"key":"150_CR14","volume-title":"Proc of PLDI\u201901","author":"A M\u00f8ller","year":"2001","unstructured":"M\u00f8ller A, Schwartzbach M (2001) The pointer assertion logic engine. In: Proc of PLDI\u201901. ACM, New York"},{"key":"150_CR15","series-title":"LNCS","volume-title":"Proc of VMCAI\u201907","author":"HH Nguyen","year":"2007","unstructured":"Nguyen HH, David C, Qin S, Chin WN (2007) Automated verification of shape and size properties via separation logic. In: Proc of VMCAI\u201907. LNCS, vol 4349. Springer, Berlin"},{"key":"150_CR16","volume-title":"Proc of LICS\u201902","author":"JC Reynolds","year":"2002","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proc of LICS\u201902. IEEE Comput Soc, Los Alamitos"},{"issue":"3","key":"150_CR17","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv S, Reps TW, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst 24(3):217\u2013298","journal-title":"ACM Trans Program Lang Syst"},{"key":"150_CR18","unstructured":"Yang H, Lee O, Calcagno C, Distefano D, O\u2019Hearn PW (2007) On scalable shape analysis. Technical report RR-07-10, Queen Mary, University of London"},{"key":"150_CR19","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1145\/1394622","volume-title":"Proc of CAV\u201908","author":"H Yang","year":"2008","unstructured":"Yang H, Lee O, Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW (2008) Scalable shape analysis for systems code. In: Proc of CAV\u201908. LNCS, vol 5123. Springer, Berlin"},{"key":"150_CR20","volume-title":"Proc of PLDI\u201908","author":"K Zee","year":"2008","unstructured":"Zee K, Kuncak V, Rinard M (2008) Full functional verification of linked data structures. In: Proc of PLDI\u201908. ACM, New York"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0150-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0150-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0150-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T15:30:39Z","timestamp":1642001439000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0150-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,11]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["150"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0150-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,4,11]]}}}