{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:53:33Z","timestamp":1725573213473},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540254355"},{"type":"electronic","value":"9783540319870"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31987-0_10","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T18:42:00Z","timestamp":1292870520000},"page":"124-140","source":"Crossref","is-referenced-by-count":32,"title":["Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis"],"prefix":"10.1007","author":[{"given":"Oukseh","family":"Lee","sequence":"first","affiliation":[]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Kwangkeun","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press and McGraw-Hill Book Company (2001)"},{"key":"10_CR2","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: Proceedings of the ACM Symposium on Principles of Programming Languages, January 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"10_CR3","doi-asserted-by":"publisher","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. Logic and Comput.\u00a02(4), 511\u2013547 (1992)","journal-title":"J. Logic and Comput."},{"key":"10_CR4","first-page":"170","volume-title":"Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture","author":"P. Cousot","year":"1995","unstructured":"Cousot, P., Cousot, R.: Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In: Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture, La Jolla, California, June 1995, pp. 170\u2013181. ACM Press, New York (1995)"},{"key":"10_CR5","first-page":"230","volume-title":"Proceedings of the ACM Conference on Programming Language Design and Implementation","author":"A. Deutsch","year":"1994","unstructured":"Deutsch, A.: Interprocedural alias analysis for pointers: Beyond k-limiting. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, pp. 230\u2013241. ACM Press, New York (1994)"},{"key":"10_CR6","first-page":"27","volume-title":"Proceedings of the ACM Symposium on Principles of Programming Languages","author":"P. Fradet","year":"1997","unstructured":"Fradet, P., Le M\u00e9tayer, D.: Shape types. In: Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 27\u201339. ACM Press, New York (1997)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proceedings of the ACM Symposium on Principles of Programming Languages (January 1993)","DOI":"10.1145\/158511.158628"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. Tech. Memo. ROPAS-2005-23, Programming Research Laboratory, School of Computer Science & Engineering, Seoul National University (March 2005)","DOI":"10.1007\/978-3-540-31987-0_10"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-27864-1_20","volume-title":"Static Analysis","author":"R. Manevich","year":"2004","unstructured":"Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 265\u2013279. Springer, Heidelberg (2004)"},{"key":"10_CR10","volume-title":"Proceedings of the ACM Conference on Programming Language Design and Implementation","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proceedings of the ACM Conference on Programming Language Design and Implementation. ACM, New York (2001)"},{"key":"10_CR11","first-page":"268","volume-title":"Proceedings of the ACM Symposium on Principles of Programming Languages","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 268\u2013280. ACM Press, New York (2004)"},{"key":"10_CR12","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Proceedings of the 17th IEEE Symposium on Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE, Los Alamitos (2002)"},{"issue":"1","key":"10_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst.\u00a020(1), 1\u201350 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"10_CR14","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-27815-3_36","volume-title":"Algebraic Methodology and Software Technology","author":"\u00c9.-J. Sims","year":"2004","unstructured":"Sims, \u00c9.-J.: Extending separation logic with fixpoints and postponed substitution. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 475\u2013490. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31987-0_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:33:16Z","timestamp":1605760396000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31987-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540254355","9783540319870"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31987-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}