{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:00:57Z","timestamp":1725796857447},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319091075"},{"type":"electronic","value":"9783319091082"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09108-2_4","type":"book-chapter","created":{"date-parts":[[2014,7,4]],"date-time":"2014-07-04T09:07:01Z","timestamp":1404464821000},"page":"49-64","source":"Crossref","is-referenced-by-count":3,"title":["Generating Abstract Graph-Based Procedure Summaries for Pointer Programs"],"prefix":"10.1007","author":[{"given":"Christina","family":"Jansen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL 2005, pp. 259\u2013270. ACM (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"4_CR3","unstructured":"Dodds, M., Plump, D.: From hyperedge replacement to separation logic and back. In: Proc. Doctoral Symp. at the Int. Conf. on Graph Transformation, ICGT 2008. Electronic Communications of the EASST, vol.\u00a016 (2009)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/3-540-61055-3_33","volume-title":"Programming Languages and Systems - ESOP \u201996","author":"P. Fradet","year":"1996","unstructured":"Fradet, P., Caugne, R., M\u00e9tayer, D.L.: Static detection of pointer errors: An axiomatisation and a checking algorithm. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol.\u00a01058, pp. 125\u2013140. Springer, Heidelberg (1996)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11823230_16","volume-title":"Static Analysis","author":"A. Gotsman","year":"2006","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 240\u2013260. Springer, Heidelberg (2006)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI 2007, pp. 266\u2013277. ACM Press (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"G\u00fcldali, B., Mlynarski, M., W\u00fcbbeke, A., Engels, G.: Model-based system testing using visual contracts. In: 35th Euromicro Conf. on Software Engineering and Advanced Applications (SEAA 2009), pp. 121\u2013124 (August 2009)","DOI":"10.1109\/SEAA.2009.42"},{"key":"4_CR8","first-page":"13","volume":"15","author":"C. Haack","year":"2011","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica\u00a015, 13\u201323 (2011)","journal-title":"Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-31762-0_10","volume-title":"Formal Verification of Object-Oriented Software","author":"J. Heinen","year":"2012","unstructured":"Heinen, J., Barthels, H., Jansen, C.: Juggrnaut \u2013 an abstract JVM. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 142\u2013159. Springer, Heidelberg (2012)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Heinen, J., Noll, T., Rieger, S.: Juggrnaut: Graph grammar abstraction for unbounded heap structures. In: Proc. 3rd Int. Workshop on Harnessing Theories for Tool Support in Software. ENTCS, vol.\u00a0266, pp. 93\u2013107. Elsevier (2010)","DOI":"10.1016\/j.entcs.2011.07.001"},{"key":"4_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-38574-2_2","volume-title":"Automated Deduction \u2013 CADE-24","author":"R. Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol.\u00a07898, pp. 21\u201338. Springer, Heidelberg (2013)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Jansen, C., G\u00f6be, F., Noll, T.: Generating inductive predicates for symbolic execution of pointer-manipulating programs (submitted, 2014)","DOI":"10.1007\/978-3-319-09108-2_5"},{"key":"4_CR13","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.\u00a06638, pp. 323\u2013335. Springer, Heidelberg (2011)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/3-540-55984-1_13","volume-title":"Compiler Construction","author":"J. Knoop","year":"1992","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol.\u00a0641, pp. 125\u2013140. Springer, Heidelberg (1992)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Kreiker, J., Reps, T., Rinetzky, N., Sagiv, M., Wilhelm, R., Yahav, E.: Interprocedural shape analysis for effectively cutpoint-free programs. In: Voronkov, A., Weidenbach, C. (eds.) Ganzinger Festschrift. LNCS, vol.\u00a07797, pp. 414\u2013445. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37651-1_17"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-68237-0_8","volume-title":"FM 2008: Formal Methods","author":"T.G. Noll","year":"2008","unstructured":"Noll, T.G., Rieger, S.: Verifying dynamic pointer-manipulating threads. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 84\u201399. Springer, Heidelberg (2008)"},{"key":"4_CR17","unstructured":"Plump, D.: Checking graph-transformation systems for confluence. ECEASST 26 (2010)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proc. 22nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 1995, pp. 49\u201361. ACM Press (1995)","DOI":"10.1145\/199448.199462"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-45306-7_10","volume-title":"Compiler Construction","author":"N. Rinetzky","year":"2001","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol.\u00a02027, pp. 133\u2013149. Springer, Heidelberg (2001)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/11547662_20","volume-title":"Static Analysis","author":"N. Rinetzky","year":"2005","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural shape analysis for cutpoint-free programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 284\u2013302. Springer, Heidelberg (2005)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. In: Mosses, P.D., Nielsen, M. (eds.) TAPSOFT 1995. LNCS, vol.\u00a0915, pp. 651\u2013665. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-59293-8_226"},{"key":"4_CR22","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189\u2013233. Prentice-Hall (1981)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Yahav, E., Chandra, S.: Generating precise and concise procedure summaries. In: Proc. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 221\u2013234. ACM Press (2008)","DOI":"10.1145\/1328438.1328467"}],"container-title":["Lecture Notes in Computer Science","Graph Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09108-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T02:55:29Z","timestamp":1558925729000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09108-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319091075","9783319091082"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09108-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}