{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T01:34:27Z","timestamp":1768354467296,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319929699","type":"print"},{"value":"9783319929705","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92970-5_17","type":"book-chapter","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T08:54:12Z","timestamp":1527584052000},"page":"271-286","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Graph-Based Shape Analysis Beyond Context-Freeness"],"prefix":"10.1007","author":[{"given":"Hannah","family":"Arndt","sequence":"first","affiliation":[]},{"given":"Christina","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"issue":"4","key":"17_CR1","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/s00236-015-0235-0","volume":"53","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Hol\u00edk, L., Jonsson, B., Leng\u00e1l, O., Trinh, C.Q., Vojnar, T.: Verification of heap manipulating programs with ordered data by extended forest automata. Acta Inf. 53(4), 357\u2013385 (2016)","journal-title":"Acta Inf."},{"issue":"4","key":"17_CR2","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1145\/321479.321488","volume":"15","author":"AV Aho","year":"1968","unstructured":"Aho, A.V.: Indexed grammars - an extension of context-free grammars. J. ACM 15(4), 647\u2013671 (1968)","journal-title":"J. ACM"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Arndt, H., Jansen, C., Katoen, J.P., Matheja, C., Noll, T.: Let this graph be your witness! an attestor for verifying Java pointer programs. In: CAV (2018, to appear)","DOI":"10.1007\/978-3-319-96142-2_1"},{"key":"17_CR4","unstructured":"Arndt, H., Jansen, C., Matheja, C., Noll, T.: Heap abstraction beyond context-freeness. CoRR abs\/1705.03754 (2017). http:\/\/arxiv.org\/abs\/1705.03754"},{"key":"17_CR5","first-page":"143","volume":"14","author":"Y Bar-Hillel","year":"1961","unstructured":"Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Sprachtypologie und Universalienforschung 14, 143\u2013172 (1961)","journal-title":"Sprachtypologie und Universalienforschung"},{"issue":"6","key":"17_CR6","doi-asserted-by":"crossref","first-page":"26:1","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011)","journal-title":"J. ACM"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Chang, B.E., Rival, X.: Relational inductive shape analysis. In: POPL 2008, pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"17_CR8","doi-asserted-by":"crossref","first-page":"161","DOI":"10.4204\/EPTCS.129.11","volume":"129","author":"BE Chang","year":"2013","unstructured":"Chang, B.E., Rival, X.: Modular construction of shape-numeric analyzers. EPTCS 129, 161\u2013185 (2013)","journal-title":"EPTCS"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B-YE Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_24"},{"issue":"9","key":"17_CR10","doi-asserted-by":"crossref","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W Chin","year":"2012","unstructured":"Chin, W., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"17_CR12","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511\u2013547 (1992)","journal-title":"J. Log. Comput."},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-33826-7_5","volume-title":"Software Engineering and Formal Methods","author":"P Ferrara","year":"2012","unstructured":"Ferrara, P., Fuchs, R., Juhasz, U.: TVAL+ : TVLA and value analyses together. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 63\u201377. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_5"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013875","volume-title":"Hyperedge Replacement: Grammars and Languages","author":"A Habel","year":"1992","unstructured":"Habel, A.: Hyperedge Replacement: Grammars and Languages. LNCS, vol. 643. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0013875"},{"issue":"2","key":"17_CR15","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/s10703-015-0236-1","volume":"47","author":"J Heinen","year":"2015","unstructured":"Heinen, J., Jansen, C., Katoen, J., Noll, T.: Juggrnaut: using graph grammars for abstracting unbounded heap structures. Form. Method. Syst. Des. 47(2), 159\u2013203 (2015)","journal-title":"Form. Method. Syst. Des."},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-09108-2_5","volume-title":"Graph Transformation","author":"C Jansen","year":"2014","unstructured":"Jansen, C., G\u00f6be, F., Noll, T.: Generating Inductive predicates for symbolic execution of pointer-manipulating programs. In: Giese, H., K\u00f6nig, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 65\u201380. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09108-2_5"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-642-21254-3_25","volume-title":"Language and Automata Theory and Applications","author":"C Jansen","year":"2011","unstructured":"Jansen, C., Heinen, J., Katoen, J.-P., Noll, T.: A local Greibach normal form for hyperedge replacement grammars. In: Dediu, A.-H., Inenaga, S., Mart\u00edn-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 323\u2013335. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21254-3_25"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/978-3-662-54434-1_23","volume-title":"Programming Languages and Systems","author":"C Jansen","year":"2017","unstructured":"Jansen, C., Katelaan, J., Matheja, C., Noll, T., Zuleger, F.: Unified reasoning about robustness properties of symbolic-heap separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 611\u2013638. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_23"},{"key":"17_CR19","unstructured":"Plump, D.: Checking graph-transformation systems for confluence. In: ECEASST, vol. 26 (2010)"},{"key":"17_CR20","volume-title":"The Compiler Design Handbook","author":"TW Reps","year":"2007","unstructured":"Reps, T.W., Sagiv, M., Wilhelm, R.: Shape analysis and applications. In: Srikant, Y.N., Shankar, P. (eds.) The Compiler Design Handbook, 2nd edn. CRC Press, Boca Raton (2007)","edition":"2"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL 1999, pp. 105\u2013118. ACM (1999)","DOI":"10.1145\/292540.292552"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92970-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T15:23:55Z","timestamp":1571412235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92970-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929699","9783319929705"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92970-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}