{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T14:59:30Z","timestamp":1782572370942,"version":"3.54.5"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,9,4]],"date-time":"2015-09-04T00:00:00Z","timestamp":1441324800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission (BE)","doi-asserted-by":"publisher","award":["287767"],"award-info":[{"award-number":["287767"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,10]]},"DOI":"10.1007\/s10703-015-0236-1","type":"journal-article","created":{"date-parts":[[2015,9,4]],"date-time":"2015-09-04T05:23:17Z","timestamp":1441344197000},"page":"159-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Juggrnaut: using graph grammars for abstracting unbounded heap structures"],"prefix":"10.1007","volume":"47","author":[{"given":"Jonathan","family":"Heinen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christina","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,9,4]]},"reference":[{"key":"236_CR1","doi-asserted-by":"crossref","unstructured":"Bals M, Jansen C, Noll T (2013) Incremental construction of Greibach normal form for context-free grammars. In: International symposium on theoretical aspects of software engineering (TASE 2013), IEEE CS Press, pp 165\u2013168","DOI":"10.1109\/TASE.2013.42"},{"key":"236_CR2","doi-asserted-by":"crossref","unstructured":"Berdine J, Calcagno C, O\u2019Hearn PW (2004) A decidable fragment of separation logic. In: 24th International conference on foundations of software technology and theoretical computer science (FSTTCS), Springer, LNCS, vol 3328, pp 97\u2013109","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"236_CR3","unstructured":"Berdine J, Calcagno C, O\u2019Hearn PW (2005) Smallfoot: modular automatic assertion checking with separation logic. In: Formal methods for components and objects, Springer, LNCS, vol 4111, pp 115\u2013137"},{"key":"236_CR4","doi-asserted-by":"crossref","unstructured":"Bhat G, Cleaveland R, Grumberg O (1995) Efficient on-the-fly model checking for CTL*. In: 10th Annual IEEE symposium on logic in computer science, pp 388\u2013397","DOI":"10.1109\/LICS.1995.523273"},{"key":"236_CR5","doi-asserted-by":"crossref","unstructured":"Bogudlov I, Lev-Ami T, Reps TW, Sagiv M (2007) Revamping TVLA: making parametric shape analysis competitive. In: 19th International conference on computer aided verification (CAV), Springer, LNCS, vol 4590, pp 221\u2013225","DOI":"10.1007\/978-3-540-73368-3_25"},{"key":"236_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Bozga M, Habermehl P, Iosif R, Moro P, Vojnar T (2006a) Programs with lists are counter automata. In: 18th international conference on computer-aided verification (CAV), Springer, LNCS, vol 4144, pp 517\u2013531","DOI":"10.1007\/11817963_47"},{"key":"236_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Habermehl P, Rogalewicz A, Vojnar T (2006b) Abstract regular tree model checking of complex dynamic data structures. In: Static analysis symposium (SAS), Springer, LNCS, vol 4134, pp 52\u201370","DOI":"10.1007\/11823230_5"},{"issue":"1","key":"236_CR8","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1016\/0890-5401(90)90043-H","volume":"85","author":"B Courcelle","year":"1990","unstructured":"Courcelle B (1990) The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf Comput 85(1):12\u201375","journal-title":"Inf Comput"},{"key":"236_CR9","first-page":"313","volume-title":"Handbook of graph grammars","author":"B Courcelle","year":"1997","unstructured":"Courcelle B (1997) The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg G (ed) Handbook of graph grammars. Singapore, Singapore, pp 313\u2013400"},{"key":"236_CR10","unstructured":"Distefano D, Katoen JP, Rensink A (2005) Safety and liveness in concurrent pointer programs. In: Formal methods for components and objects, Springer, LNCS, vol 4111, pp 280\u2013312"},{"key":"236_CR11","unstructured":"Dodds M, Plump D (2009) From hyperedge replacement to separation logic and back. ECEASST 16, http:\/\/journal.ub.tu-berlin.de\/index.php\/eceasst\/article\/view\/237\/236"},{"key":"236_CR12","first-page":"95","volume-title":"Handbook of graph grammars","author":"F Drewes","year":"1997","unstructured":"Drewes F, Kreowski HJ, Habel A (1997) Hyperedge replacement graph grammars. In: Rozenberg G (ed) Handbook of graph grammars. World Scientific, Singapore, pp 95\u2013162"},{"key":"236_CR13","doi-asserted-by":"crossref","unstructured":"Elgaard J, M\u00f8ller A, Schwartzbach MI (2000) Compile-time debugging of C programs working on trees. In: Programming languages and systems, LNCS, vol 1782, Springer, pp 119\u2013134","DOI":"10.1007\/3-540-46425-5_8"},{"key":"236_CR14","doi-asserted-by":"crossref","unstructured":"Engelfriet J (1992) A Greibach normal form for context-free graph grammars. In: International conference on automata, languages and programming (ICALP), Springer, LNCS, vol 623, pp 138\u2013149","DOI":"10.1007\/3-540-55719-9_70"},{"key":"236_CR15","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/s10009-011-0186-x","volume":"14","author":"AH Ghamarian","year":"2012","unstructured":"Ghamarian AH, de Mol MJ, Rensink A, Zambon E, Zimakova MV (2012) Modelling and analysis using GROOVE. Int J Softw Tools Technol Transf 14:15\u201340","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"1\u20132","key":"236_CR16","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/BF01917434","volume":"8","author":"R Halin","year":"1976","unstructured":"Halin R (1976) S-functions for graphs. J Geom 8(1\u20132):171\u2013186","journal-title":"J Geom"},{"key":"236_CR17","unstructured":"Heinen J (2015) Verifying Java programs\u2014a graph grammar approach. PhD thesis, RWTH Aachen University, Germany"},{"key":"236_CR18","doi-asserted-by":"crossref","unstructured":"Heinen J, Noll T, Rieger S (2010) Juggrnaut: graph grammar abstraction for unbounded heap structures. In: Proceedings of the 3rd international workshop on harnessing theories for tool support in software (TTSS 2009), Elsevier, ENTCS, vol 266, pp 93\u2013107","DOI":"10.1016\/j.entcs.2011.07.001"},{"key":"236_CR19","doi-asserted-by":"crossref","unstructured":"Heinen J, Barthels H, Jansen C (2012) Juggrnaut\u2014an abstract JVM. In: Formal verification of object-oriented software (FoVeOOS\u00a02011), Springer, LNCS, vol 7421, pp 142\u2013159","DOI":"10.1007\/978-3-642-31762-0_10"},{"key":"236_CR20","doi-asserted-by":"crossref","DOI":"10.1201\/b10690","volume-title":"Fundamentals of mathematical logic","author":"P Hinman","year":"2005","unstructured":"Hinman P (2005) Fundamentals of mathematical logic. A.K. Peters Ltd, Wellesley"},{"key":"236_CR21","doi-asserted-by":"crossref","unstructured":"Iosif R, Rogalewicz A, Simacek J (2013) The tree width of separation logic with recursive definitions. In: Automated deduction (CADE-24) (Lecture notes in computer science), vol 7898, Springer, pp 21\u201338","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"236_CR22","doi-asserted-by":"crossref","unstructured":"Jansen C, Noll T (2014) Generating abstract graph-based procedure summaries for pointer programs. In: Graph transformations (ICGT 2014), Springer, LNCS, vol 8571, pp 49\u201364","DOI":"10.1007\/978-3-319-09108-2_4"},{"key":"236_CR23","doi-asserted-by":"crossref","unstructured":"Jansen C, Heinen J, Katoen JP, Noll T (2011) A local Greibach normal form for hyperedge replacement grammars. In: 5th international conference on language and automata theory and applications (LATA 2011), Springer, LNCS, vol 6638, pp 323\u2013335","DOI":"10.1007\/978-3-642-21254-3_25"},{"key":"236_CR24","doi-asserted-by":"crossref","unstructured":"Jansen C, G\u00f6be F, Noll T (2014) Generating inductive predicates for symbolic execution of pointer-manipulating programs. In: Graph transformation (ICGT 2014), Springer, LNCS, vol 8571, pp 65\u201380","DOI":"10.1007\/978-3-319-09108-2_5"},{"key":"236_CR25","doi-asserted-by":"crossref","unstructured":"Jensen JL, J\u00f8rgensen ME, Schwartzbach MI, Klarlund N (1997) Automatic verification of pointer programs using monadic second-order logic. In: ACM SIGPLAN 1997 conference on programming language design and implementation (PLDI \u201997), ACM Press, pp 226\u2013234","DOI":"10.1145\/258915.258936"},{"key":"236_CR26","doi-asserted-by":"crossref","unstructured":"Klarlund N, M\u00f8ller A, Schwartzbach MI (2001) Mona implementation secrets. In: Implementation and application of automata, LNCS, vol 2088, Springer, pp 182\u2013194","DOI":"10.1007\/3-540-44674-5_15"},{"key":"236_CR27","doi-asserted-by":"crossref","unstructured":"Lee O, Yang H, Yi K (2005) Automatic verification of pointer programs using grammar-based shape analysis. In: Proceedings of 14th European symposium on programming (ESOP \u201905), Springer, LNCS, vol 3444, pp 124\u2013140","DOI":"10.1007\/978-3-540-31987-0_10"},{"issue":"2","key":"236_CR28","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0020-0190(73)90012-4","volume":"2","author":"G Lindstrom","year":"1973","unstructured":"Lindstrom G (1973) Scanning list structures without stacks or tag bits. Inf Process Lett 2(2):47\u201351","journal-title":"Inf Process Lett"},{"key":"236_CR29","doi-asserted-by":"crossref","unstructured":"Loginov A, Reps TW, Sagiv M (2006) Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: 13th International static analysis symposium (SAS), Springer, LNCS, vol 4134, pp 261\u2013279","DOI":"10.1007\/11823230_17"},{"key":"236_CR30","doi-asserted-by":"crossref","unstructured":"Madhusudan P, Qiu X (2011) Efficient decision procedures for heaps using STRAND. In: Static analysis, LNCS, vol 6887, Springer, pp 43\u201359","DOI":"10.1007\/978-3-642-23702-7_8"},{"key":"236_CR31","doi-asserted-by":"crossref","unstructured":"Madhusudan P, Parlato G, Qiu X (2011) Decidable logics combining heap structures and data. In: POPL 2011, ACM Press, pp 611\u2013622","DOI":"10.1145\/1926385.1926455"},{"issue":"1\u20132","key":"236_CR32","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F Mehta","year":"2005","unstructured":"Mehta F, Nipkow T (2005) Proving pointer programs in higher-order logic. Inf Comput 199(1\u20132):200\u2013227","journal-title":"Inf Comput"},{"key":"236_CR33","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn PW, Yang H, Reynolds JC (2004) Separation and information hiding. In: ACM symposium on principles of programming languages (POPL), ACM Press, pp 268\u2013280","DOI":"10.1145\/964001.964024"},{"key":"236_CR34","unstructured":"Plump D (2010) Checking graph-transformation systems for confluence. ECEASST 26, http:\/\/journal.ub.tu-berlin.de\/eceasst\/article\/view\/367\/347"},{"key":"236_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, IEEE CS Press, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"236_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-2011-615","volume":"114","author":"C Poskitt","year":"2012","unstructured":"Poskitt C, Plump D (2012) Hoare-style verification of graph programs. Fundam Inf 114:1\u201343","journal-title":"Fundam Inf"},{"key":"236_CR37","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: IEEE symposium on logic in computer science (LICS), IEEE CS Press, pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"236_CR38","doi-asserted-by":"crossref","unstructured":"Rieger S, Noll T (2008) Abstracting complex data structures by hyperedge replacement. In: 4th international conference on graph transformations (ICGT 2008), Springer, LNCS, vol 5214, pp 69\u201383","DOI":"10.1007\/978-3-540-87405-8_6"},{"issue":"3","key":"236_CR39","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 TOPLAS 24(3):217\u2013298","journal-title":"ACM TOPLAS"},{"key":"236_CR40","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1145\/363534.363554","volume":"10","author":"H Schorr","year":"1967","unstructured":"Schorr H, Waite WM (1967) An efficient machine-independent procedure for garbage collection in various list structures. Commun ACM 10:501\u2013506","journal-title":"Commun ACM"},{"key":"236_CR41","doi-asserted-by":"crossref","unstructured":"Yang H, Lee O, Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW (2008) Scalable shape analysis for systems code. In: 20th international conference on computer aided verification (CAV), Springer, LNCS, vol 5123, pp 385\u2013398","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"236_CR42","doi-asserted-by":"crossref","unstructured":"Yuasa Y, Tanabe Y, Sekizawa T, Takahashi K (2008) Verification of the Deutsch-Schorr-Waite marking algorithm with modal logic. In: 2nd international conference on verified software: theories, tools, experiments (VSTTE), Springer, LNCS, vol 5295, pp 115\u2013129","DOI":"10.1007\/978-3-540-87873-5_12"},{"key":"236_CR43","unstructured":"Zambon E (2013) Abstract graph transformation\u2014theory and practice. PhD thesis, University of Twente"},{"key":"236_CR44","doi-asserted-by":"crossref","unstructured":"Zambon E, Rensink A (2012) Graph subsumption in abstract state space exploration. In: Graph inspection and traversal engineering (GRAPHite 2012), Electronic proceedings in theoretical computer science, vol 99, pp 35\u201349","DOI":"10.4204\/EPTCS.99.6"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0236-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0236-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0236-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T00:24:55Z","timestamp":1599524695000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0236-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,4]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,10]]}},"alternative-id":["236"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0236-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,4]]}}}