{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:15Z","timestamp":1725494415462},"publisher-location":"Berlin, Heidelberg","reference-count":32,"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_17","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T07:58:07Z","timestamp":1194854287000},"page":"234-250","source":"Crossref","is-referenced-by-count":3,"title":["Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning"],"prefix":"10.1007","author":[{"given":"Sigmund","family":"Cherem","sequence":"first","affiliation":[]},{"given":"Radu","family":"Rugina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46423-9_1","volume-title":"Compiler Construction","author":"R. Wilhelm","year":"2000","unstructured":"Wilhelm, R., Sagiv, M., Reps, T.: Shape analysis. In: Watt, D.A. (ed.) CC 2000 and ETAPS 2000. LNCS, vol.\u00a01781, Springer, Heidelberg (2000)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Lev-ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Proceedings of the 2000 International Symposium on Software Testing and Analysis (2000)","DOI":"10.1145\/347324.348031"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0026429","volume-title":"Compiler Construction","author":"R. Ghiya","year":"1998","unstructured":"Ghiya, R., Hendren, L., Zhu, Y.: Detecting parallelism in C programs with recursive data structures. In: Koskimies, K. (ed.) CC 1998 and ETAPS 1998. LNCS, vol.\u00a01383, Springer, Heidelberg (1998)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: Proceedings of the 32th Annual ACM Symposium on the Principles of Programming Languages, Long Beach, CA (2005)","DOI":"10.1145\/1040305.1040331"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Cherem, S., Rugina, R.: Compile-time deallocation of individual objects. In: Proceedings of the International Symposium on Memory Management, Ottawa, Canada (2006)","DOI":"10.1145\/1133956.1133975"},{"issue":"1","key":"17_CR6","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 Transactions on Programming Languages and Systems\u00a020(1), 1\u201350 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2005)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, Springer, Heidelberg (2006)"},{"key":"17_CR10","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":"17_CR11","unstructured":"Cherem, S., Rugina, R.: Maintaining structural invariants in shape analysis with local reasoning. TR CS TR2006-2048, Cornell University (2006)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, Springer, Heidelberg (2000)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Jones, N., Muchnick, S.: Flow analysis and optimization of Lisp-like structures. In: Conference Record of the 6th Annual ACM Symposium on the Principles of Programming Languages, San Antonio, TX (1979)","DOI":"10.1145\/567752.567776"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Chase, D., Wegman, M., Zadek, F.: Analysis of pointers and structures. In: Proceedings of the SIGPLAN \u201991 Conference on Program Language Design and Implementation, White Plains, NY (1990)","DOI":"10.1145\/93542.93585"},{"issue":"1","key":"17_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1109\/71.80123","volume":"1","author":"L. Hendren","year":"1990","unstructured":"Hendren, L., Nicolau, A.: Parallelizing programs with recursive data structures. IEEE Transactions on Parallel and Distributed Systems\u00a01(1), 35\u201347 (1990)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Hendren, L., Hummel, J., Nicolau, A.: A general data dependence test for dynamic, pointer-based data structures. In: Proceedings of the SIGPLAN \u201994 Conference on Program Language Design and Implementation, Orlando, FL (1994)","DOI":"10.1145\/178243.178262"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: Proceedings of the SIGPLAN \u201994 Conference on Program Language Design and Implementation, Orlando, FL (1994)","DOI":"10.1145\/178243.178263"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Ghiya, R., Hendren, L.: Is is a tree, a DAG or a cyclic graph? A shape analysis for heap-directed pointers in C. In: Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages, St. Petersburg Beach, FL (1996)","DOI":"10.1145\/237721.237724"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_26","volume-title":"Static Analysis","author":"S. Chong","year":"2003","unstructured":"Chong, S., Rugina, R.: Static analysis of accessed regions in recursive data structures. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"17_CR20","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":"17_CR21","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. In: Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages, St. Petersburg Beach, FL (1996)","DOI":"10.1145\/237721.237725"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings of the 26th Annual ACM Symposium on the Principles of Programming Languages, San Antonio, TX (1999)","DOI":"10.1145\/292540.292552"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 and ETAPS 2001. LNCS, vol.\u00a02027, Springer, Heidelberg (2001)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Moller, A., Schwartzbach, M.: The pointer assertion logic engine. In: Proceedings of the SIGPLAN \u201901 Conference on Program Language Design and Implementation, Snowbird, UT (2001)","DOI":"10.1145\/378795.378851"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.: Data structure specification via local equality axioms. In: Proceedings of the 2005 Conference on Computer-Aided Verification, Seattle, WA (2005)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Qadeer, S.: Verifying properties of well-founded linked lists. In: Proceedings of the 33th Annual ACM Symposium on the Principles of Programming Languages, Charleston, SC (2006)","DOI":"10.1145\/1111037.1111048"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of the SIGPLAN \u201901 Conference on Program Language Design and Implementation, Snowbird, UT (2001)","DOI":"10.1145\/378795.378846"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","first-page":"310","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2002","unstructured":"Dams, D., Namjoshi, K.S.: Shape analysis through predicate abstraction and model checking. In: Zuck, L.D., et al. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 310\u2013324. Springer, Heidelberg (2002)"},{"key":"17_CR30","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.D. Bingham","year":"2005","unstructured":"Bingham, J.D., 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)"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th Annual ACM Symposium on the Principles of Programming Languages, London, UK (2001)","DOI":"10.1145\/360204.375719"}],"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_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:45:04Z","timestamp":1620002704000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_17","relation":{},"subject":[]}}