{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:10:24Z","timestamp":1763467824241},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_18","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"251-266","source":"Crossref","is-referenced-by-count":60,"title":["Automated Verification of Shape and Size Properties Via Separation Logic"],"prefix":"10.1007","author":[{"given":"Huu Hai","family":"Nguyen","sequence":"first","affiliation":[]},{"given":"Cristina","family":"David","sequence":"additional","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, Springer, Heidelberg (2005)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., et al. (eds.) FMCO 2005. LNCS, vol.\u00a04111, Springer, Heidelberg (2006)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11609773_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Bingham","year":"2005","unstructured":"Bingham, J., Rakamaric, Z.: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 207\u2013221. Springer, Heidelberg (2005)"},{"issue":"1","key":"18_CR4","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R.M. Burstall","year":"1977","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of ACM\u00a024(1), 44\u201367 (1977)","journal-title":"Journal of ACM"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: ACM SIGPLAN ICFP, Tallinn, Estonia (September 2005)","DOI":"10.1145\/1086365.1086375"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Chin, W.N., Khoo, S.C.: Calculating sized types. In: ACM SIGPLAN PEPM, pp. 62\u201372, Boston, United States (January 2000)","DOI":"10.1145\/328691.328893"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Chin, W.N., Khoo, S.C., Qin, S.C., Popeea, C., Nguyen, H.H.: Verifying Safety Policies with Size Properties and Alias Controls. In: ACM SIGSOFT ICSE, St. Louis, Missouri (May 2005)","DOI":"10.1145\/1062455.1062500"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"key":"18_CR9","first-page":"410","volume-title":"ACM POPL","author":"J. Hughes","year":"1996","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: ACM POPL, pp. 410\u2013423. ACM Press, New York (1996)"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Isthiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL, London (January 2001)","DOI":"10.1145\/360204.375719"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_10","volume-title":"Programming Languages and Systems","author":"L. Jia","year":"2006","unstructured":"Jia, L., Walker, D.: ILC: A foundation for automated reasoning about pointer programs. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, Springer, Heidelberg (2006)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"O. Lee","year":"2005","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, Springer, Heidelberg (2005)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: ACM POPL, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Moeller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: ACM PLDI, (June 2001)","DOI":"10.1145\/378795.378851"},{"key":"18_CR15","unstructured":"Nguyen, H.H., et al.: Automated Verification of Shape and Size Properties via Separation Logic. Technical report, SoC, Natl Univ. of Singapore (July 2006), available at http:\/\/www.comp.nus.edu.sg\/~nguyenh2\/papers\/vmcai07-report.pdf"},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a08, 102\u2013114 (1992)","journal-title":"Communications of the ACM"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: IEEE LICS, Copenhagen, Denmark (July 2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b96957","volume-title":"Static Analysis","author":"R. Rugina","year":"2004","unstructured":"Rugina, R.: Quantitative Shape Analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, Springer, Heidelberg (2004)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24(3) (2002)","DOI":"10.1145\/514188.514190"},{"issue":"2","key":"18_CR20","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.tcs.2005.09.071","volume":"351","author":"\u00c9.-J. Sims","year":"2006","unstructured":"Sims, \u00c9.-J.: Extending separation logic with fixpoints and postponed substitution. Theoretical Computer Science\u00a0351(2), 258\u2013275 (2006)","journal-title":"Theoretical Computer Science"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/3-540-45332-6_7","volume-title":"Types in Compilation","author":"D. Walker","year":"2001","unstructured":"Walker, D., Morrisett, G.: Alias Types for Recursive Data Structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol.\u00a02071, pp. 177\u2013206. Springer, Heidelberg (2001)"},{"key":"18_CR22","unstructured":"Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University (1998)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:45:05Z","timestamp":1620017105000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_18","relation":{},"subject":[]}}