{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T02:50:30Z","timestamp":1761706230305},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2007,1]]},"abstract":"<jats:p>Shape analysis concerns the problem of determining \u201cshape invariants\u201d for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed using an abstract interpretation based on three-valued first-order logic. In that work, concrete stores are finite two-valued logical structures, and the sets of stores that can possibly arise during execution are represented (conservatively) using a certain family of finite three-valued logical structures. In this article, we show how three-valued structures that arise in shape analysis can be characterized using formulas in first-order logic with transitive closure. We also define a nonstandard (\u201csupervaluational\u201d) semantics for three-valued first-order logic that is more precise than a conventional three-valued semantics, and demonstrate that the supervaluational semantics can be implemented using existing theorem provers.<\/jats:p>","DOI":"10.1145\/1182613.1182618","type":"journal-article","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T19:20:08Z","timestamp":1175800808000},"page":"5","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Logical characterizations of heap abstractions"],"prefix":"10.1145","volume":"8","author":[{"given":"Greta","family":"Yorsh","sequence":"first","affiliation":[{"name":"Tel-Aviv University, Tel-Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, WI"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel-Aviv University, Tel-Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard","family":"Wilhelm","sequence":"additional","affiliation":[{"name":"Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,1]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/154630.154636"},{"key":"e_1_2_2_2_1","volume-title":"Proceedings of the European Symposium On Programming. 2--19","author":"Benedikt M.","unstructured":"Benedikt , M. , Reps , T. , and Sagiv , M . 1999. A decidable logic for describing linked data structures . In Proceedings of the European Symposium On Programming. 2--19 .]] Benedikt, M., Reps, T., and Sagiv, M. 1999. A decidable logic for describing linked data structures. In Proceedings of the European Symposium On Programming. 2--19.]]"},{"key":"e_1_2_2_3_1","volume-title":"Handbook of Philosophical Logic, 2nd. ed.","author":"Blamey S.","unstructured":"Blamey , S. 2002. Partial logic . In Handbook of Philosophical Logic, 2nd. ed. , vol. 5 , D. Gabbay and F. Guenthner, Eds . Kluwer Academic . 261--353.]] Blamey, S. 2002. Partial logic. In Handbook of Philosophical Logic, 2nd. ed., vol. 5, D. Gabbay and F. Guenthner, Eds. Kluwer Academic. 261--353.]]"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the Concurrency Theory: 11th International Conference (CONCUR). Lecture Notes in Computer Science","volume":"1877","author":"Bruns G.","unstructured":"Bruns , G. and Godefroid , P . 2000. Generalized model checking: Reasoning about partial state spaces . In Proceedings of the Concurrency Theory: 11th International Conference (CONCUR). Lecture Notes in Computer Science , vol. 1877 . Springer Verlag, 168--182.]] Bruns, G. and Godefroid, P. 2000. Generalized model checking: Reasoning about partial state spaces. In Proceedings of the Concurrency Theory: 11th International Conference (CONCUR). Lecture Notes in Computer Science, vol. 1877. Springer Verlag, 168--182.]]"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93585"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_2_8_1","volume-title":"Descriptive Complexity and Finite Models: Proceedings of a DIAMCS Workshop, N. Immerman and P. Kolaitis, Eds. American Mathematical Society. 33--57","author":"Courcelle B.","year":"1996","unstructured":"Courcelle , B. 1996 . On the expression of graph properties in some fragments of monadic second-order logic . In Descriptive Complexity and Finite Models: Proceedings of a DIAMCS Workshop, N. Immerman and P. Kolaitis, Eds. American Mathematical Society. 33--57 .]] Courcelle, B. 1996. On the expression of graph properties in some fragments of monadic second-order logic. In Descriptive Complexity and Finite Models: Proceedings of a DIAMCS Workshop, N. Immerman and P. Kolaitis, Eds. American Mathematical Society. 33--57.]]"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349309"},{"key":"e_1_2_2_13_1","unstructured":"Erez G. Sagiv M. and Yahav E. 2003. Generating concrete counter examples for arbitrary abstract domains. Unpublished manuscript.]]  Erez G. Sagiv M. and Yahav E. 2003. Generating concrete counter examples for arbitrary abstract domains. Unpublished manuscript.]]"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210112"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277667"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263706"},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the 4th Conference on Verfication, Model Checking and Abstract Interpretation (VMCAI). 206--222","author":"Godefroid P.","unstructured":"Godefroid , P. and Jagadeesan , R . 2003. On the expressiveness of 3-valued models . In Proceedings of the 4th Conference on Verfication, Model Checking and Abstract Interpretation (VMCAI). 206--222 .]] Godefroid, P. and Jagadeesan, R. 2003. On the expressiveness of 3-valued models. In Proceedings of the 4th Conference on Verfication, Model Checking and Abstract Interpretation (VMCAI). 206--222.]]"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378855"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Hell P. and Nesetril J. 2004. Graphs and Homomorphisms. Oxford University Press.]]  Hell P. and Nesetril J. 2004. Graphs and Homomorphisms. Oxford University Press.]]","DOI":"10.1093\/acprof:oso\/9780198528173.001.0001"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143138"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.80123"},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95)","author":"Henriksen J.","unstructured":"Henriksen , J. , Jensen , J. , J\u00f8rgensen , M. , Klarlund , N. , Paige , B. , Rauhe , T. , and Sandholm , A . 1996. Mona: Monadic second-order logic in practice . In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95) . 89--110.]] Henriksen, J., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., and Sandholm, A. 1996. Mona: Monadic second-order logic in practice. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95). 89--110.]]"},{"key":"e_1_2_2_24_1","volume-title":"Proceedings of the Programming Languages and Systems: 10th European Symposium on Programming (ESOP). Lecture Notes in Computer Science","volume":"2028","author":"Huth M.","unstructured":"Huth , M. , Jagadeesan , R. , and Schmidt , D. A . 2001. Modal transition systems: A foundation for three-valued program analysis . In Proceedings of the Programming Languages and Systems: 10th European Symposium on Programming (ESOP). Lecture Notes in Computer Science , vol. 2028 . Springer Verlag. 155--169.]] Huth, M., Jagadeesan, R., and Schmidt, D. A. 2001. Modal transition systems: A foundation for three-valued program analysis. In Proceedings of the Programming Languages and Systems: 10th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 2028. Springer Verlag. 155--169.]]"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Immerman N. 1999. Descriptive Complexity. Springer Verlag.]]  Immerman N. 1999. Descriptive Complexity. Springer Verlag.]]","DOI":"10.1007\/978-1-4612-0539-5"},{"key":"e_1_2_2_26_1","volume-title":"Computer Science Logic. Lecture Notes in Computer Science","volume":"3210","author":"Immerman N.","unstructured":"Immerman , N. , Rabinovich , A. , Reps , T. , Sagiv , M. , and Yorsh , G . 2004a. The boundary between decidability and undecidability for transitive-closure logics . In Computer Science Logic. Lecture Notes in Computer Science , vol. 3210 . Springer Verlag.]] Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G. 2004a. The boundary between decidability and undecidability for transitive-closure logics. In Computer Science Logic. Lecture Notes in Computer Science, vol. 3210. Springer Verlag.]]"},{"key":"e_1_2_2_27_1","volume-title":"Computer Aided Verification. Lecture Notes in Computer Science","volume":"3114","author":"Immerman N.","unstructured":"Immerman , N. , Rabinovich , A. , Reps , T. , Sagiv , M. , and Yorsh , G . 2004b. Verification via structure simulation . In Computer Aided Verification. Lecture Notes in Computer Science , vol. 3114 . Springer Verlag.]] Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G. 2004b. Verification via structure simulation. In Computer Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer Verlag.]]"},{"key":"e_1_2_2_28_1","unstructured":"Jones N. and Muchnick S. 1981. Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications S. Muchnick and N. Jones Eds. Prentice-Hall Englewood Cliffs NJ 102--131.]]  Jones N. and Muchnick S. 1981. Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications S. Muchnick and N. Jones Eds. Prentice-Hall Englewood Cliffs NJ 102--131.]]"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582161"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158628"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503276"},{"key":"e_1_2_2_32_1","volume-title":"Proceedings of the Verification Model Checking and Abstract Interpretation. Lecture Notes in Computer Science","volume":"2937","author":"Kuncak V.","unstructured":"Kuncak , V. and Rinard , M . 2003a. Boolean algebra of shape analysis constraints . In Proceedings of the Verification Model Checking and Abstract Interpretation. Lecture Notes in Computer Science , vol. 2937 . Springer Verlag. 59--72.]] Kuncak, V. and Rinard, M. 2003a. Boolean algebra of shape analysis constraints. In Proceedings of the Verification Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937. Springer Verlag. 59--72.]]"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Kuncak V. and Rinard M. 2003b. On Boolean algebra of shape analysis constraints. Tech. Rep. MIT CSAIL. http:\/\/www.mit.edu\/~vkuncak\/papers\/index.html.]]  Kuncak V. and Rinard M. 2003b. On Boolean algebra of shape analysis constraints. Tech. Rep. MIT CSAIL. http:\/\/www.mit.edu\/~vkuncak\/papers\/index.html.]]","DOI":"10.1007\/978-3-540-24622-0_7"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_16"},{"key":"e_1_2_2_35_1","unstructured":"Lev-Ami T. 2000. TVLA: A framework for Kleene based static analysis. M.S. thesis Tel-Aviv University Tel-Aviv Israel.]]  Lev-Ami T. 2000. TVLA: A framework for Kleene based static analysis. M.S. thesis Tel-Aviv University Tel-Aviv Israel.]]"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Lev-Ami T. Immerman N. Reps T. Sagiv M. Srivastava S. and Yorsh G. 2005. Simulating reachability using first-order logic with applications to verifciation of linked data structures. Submitted for publication.]]  Lev-Ami T. Immerman N. Reps T. Sagiv M. Srivastava S. and Yorsh G. 2005. Simulating reachability using first-order logic with applications to verifciation of linked data structures. Submitted for publication.]]","DOI":"10.1007\/11532231_8"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the Static Analysis Symposium. 280--301","author":"Lev-Ami T.","unstructured":"Lev-Ami , T. and Sagiv , M . 2000. TVLA: A system for implementing static analyses . In Proceedings of the Static Analysis Symposium. 280--301 .]] Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium. 280--301.]]"},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","unstructured":"McCune W. 2001. Mace 2.0 reference manual and guide. http:\/\/www-unix.mcs.anl.gov\/AR\/mace\/.]]  McCune W. 2001. Mace 2.0 reference manual and guide. http:\/\/www-unix.mcs.anl.gov\/AR\/mace\/.]]","DOI":"10.2172\/797949"},{"key":"e_1_2_2_40_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Correct Hardware Design and Venfication Methods: 110th IFIP WG 10.5 Advanced Research Working Conference (CHARME)","author":"McMillan K. L.","unstructured":"McMillan , K. L. 1999. Verification of infinite state systems by compositional model checking . In Proceedings of the Correct Hardware Design and Venfication Methods: 110th IFIP WG 10.5 Advanced Research Working Conference (CHARME) . Lecture Notes in Computer Science , vol. 1703 . Springer Verlag . 219--234.]] McMillan, K. L. 1999. Verification of infinite state systems by compositional model checking. In Proceedings of the Correct Hardware Design and Venfication Methods: 110th IFIP WG 10.5 Advanced Research Working Conference (CHARME). Lecture Notes in Computer Science, vol. 1703. Springer Verlag. 219--234.]]"},{"key":"e_1_2_2_41_1","volume-title":"Proceedings of the Symposium on Logic. 132--154","author":"Meyer A. R.","year":"1975","unstructured":"Meyer , A. R. 1975 . Weak monadic second-order theory of successor is not elementary recursive. In Logic Colloquium , Proceedings of the Symposium on Logic. 132--154 .]] Meyer, A. R. 1975. Weak monadic second-order theory of successor is not elementary recursive. In Logic Colloquium, Proceedings of the Symposium on Logic. 132--154.]]"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","unstructured":"Nielson F. Nielson H. and Hankin C. 1999. Principles of Program Analysis. Springer Verlag.]]   Nielson F. Nielson H. and Hankin C. 1999. Principles of Program Analysis. Springer Verlag.]]","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/645394.651923"},{"key":"e_1_2_2_46_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin M.","year":"1969","unstructured":"Rabin , M. 1969 . Decidability of second-order theories and automata on infinite trees . Trans. Amer. Math. Soc. 141 , 1 -- 35 .]] Rabin, M. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1--35.]]","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512540"},{"key":"e_1_2_2_48_1","volume-title":"Lecture Notes in Computer Science","volume":"2937","author":"Reps T.","unstructured":"Reps , T. , Sagiv , M. , and Yorsh , G . 2004. Symbolic implementation of the best transformer. In Verification, Model Checking, and Abstract Interpretation . Lecture Notes in Computer Science , vol. 2937 . Springer Verlag. 252--266.]] Reps, T., Sagiv, M., and Yorsh, G. 2004. Symbolic implementation of the best transformer. In Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937. Springer Verlag. 252--266.]]"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_2_52_1","volume-title":"Proceedings of the Static Analysis Symposium (SAS). Lecture Notes in Computer Science","volume":"2694","author":"Shaham R.","unstructured":"Shaham , R. , Yahav , E. , Kolodner , E. , and Sagiv , M . 2003. Establishing local temporal heap safety properties with applications to compile-time memory management . In Proceedings of the Static Analysis Symposium (SAS). Lecture Notes in Computer Science , vol. 2694 . Springer Verlag, 483--503.]] Shaham, R., Yahav, E., Kolodner, E., and Sagiv, M. 2003. Establishing local temporal heap safety properties with applications to compile-time memory management. In Proceedings of the Static Analysis Symposium (SAS). Lecture Notes in Computer Science, vol. 2694. Springer Verlag, 483--503.]]"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263703"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325706"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.2307\/2024549"},{"key":"e_1_2_2_57_1","volume-title":"SPASS: An automated theorem prover for first-order logic with equality","author":"Weidenbach C.","year":"2006","unstructured":"Weidenbach , C. 2006 . SPASS: An automated theorem prover for first-order logic with equality . http:\/\/spass.mpi-sb.mpg.de\/index.html.]] Weidenbach, C. 2006. SPASS: An automated theorem prover for first-order logic with equality. http:\/\/spass.mpi-sb.mpg.de\/index.html.]]"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360206"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996846"},{"key":"e_1_2_2_60_1","volume-title":"Electronic Notes in Theoretical Computer Science","volume":"89","author":"Yahav E.","unstructured":"Yahav , E. and Sagiv , M . 2003. Automatically verifying concurrent queue algorithms . In Electronic Notes in Theoretical Computer Science , vol. 89 . B. Cook et al. Eds. Elsevier.]] Yahav, E. and Sagiv, M. 2003. Automatically verifying concurrent queue algorithms. In Electronic Notes in Theoretical Computer Science, vol. 89. B. Cook et al. Eds. Elsevier.]]"},{"key":"e_1_2_2_62_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science","volume":"2988","author":"Yorsh G.","unstructured":"Yorsh , G. , Reps , T. W. , and Sagiv , M . 2004. Symbolically computing most precise abstract operations for shape analysis . In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science , vol. 2988 . Springer Verlag. 530--545.]] Yorsh, G., Reps, T. W., and Sagiv, M. 2004. Symbolically computing most precise abstract operations for shape analysis. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988. Springer Verlag. 530--545.]]"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1182613.1182618","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T18:55:50Z","timestamp":1672253750000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1182613.1182618"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,1]]},"references-count":58,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,1]]}},"alternative-id":["10.1145\/1182613.1182618"],"URL":"https:\/\/doi.org\/10.1145\/1182613.1182618","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,1]]},"assertion":[{"value":"2007-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}