{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:29:18Z","timestamp":1725564558634},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_7","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T07:33:53Z","timestamp":1283672033000},"page":"59-72","source":"Crossref","is-referenced-by-count":8,"title":["Boolean Algebra of Shape Analysis Constraints"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus","author":"R.-J. Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus. Springer, Heidelberg (1998)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 158. Springer, Heidelberg (2002)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for linked data structures. In: Proc. 8th ESOP (1999)","DOI":"10.1007\/3-540-49099-X_2"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Berndl, M., Lhot\u00e1k, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: PLDI 2003 (2003)","DOI":"10.1145\/781131.781144"},{"key":"7_CR6","volume-title":"ACM PLDI","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: ACM PLDI, June 2003, ACM, New York (2003)"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/777388.777395","volume-title":"ACM PEPM 2003","author":"M. Bozga","year":"2003","unstructured":"Bozga, M., Iosif, R., Laknech, Y.: Storeless semantics and alias logic. In: ACM PEPM 2003, pp. 55\u201365. ACM Press, New York (2003)"},{"issue":"7","key":"7_CR8","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W.R. Bush","year":"2000","unstructured":"Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software\u2014Practice & Experience\u00a030(7), 775\u2013802 (2000)","journal-title":"Software\u2014Practice & Experience"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Chase, D.R., Wegman, M., Kenneth Zadeck, F.: Analysis of pointers and structures. In: Proc. ACM PLDI (1990)","DOI":"10.1145\/93542.93585"},{"key":"7_CR10","volume-title":"Program Flow Analysis: Theory and Applications","author":"L. Clarke","year":"1981","unstructured":"Clarke, L., Richardson, D.: Symbolic evaluation methods for program analysis. In: Program Flow Analysis: Theory and Applications,\u00a0ch. 9, Prentice-Hall, Inc., Englewood Cliffs (1981)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-36384-X_25","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., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 310\u2013323. Springer, Heidelberg (2002)"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1145\/178243.178263","volume-title":"Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation","author":"A. Deutsch","year":"1994","unstructured":"Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, pp. 230\u2013241. ACM Pres, New York (1994)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Proc. 4th USENIX OSDI (2000)","DOI":"10.21236\/ADA419626"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Rustan, K., Leino, M., Lilibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proc. ACM PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Fradet, P., Le M\u00e9tayer, D.: Shape types. In: Proc. 24th ACM POPL (1997)","DOI":"10.1145\/263699.263706"},{"key":"7_CR16","unstructured":"Ghiya, R., Hendren, L.: Is it a tree, a DAG, or a cyclic graph? In: Proc. 23rd ACM POPL (1996)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48743-3_1","volume-title":"ECOOP \u201999 - Object-Oriented Programming","author":"C.A.R. Hoare","year":"1999","unstructured":"Hoare, C.A.R., Jifeng, H.: A trace model for pointers and objects. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol.\u00a01628, p. 1. Springer, Heidelberg (1999)"},{"key":"7_CR19","unstructured":"Holzmann, G.J.: Static source code checking for user-defined properties. In: Proc. IDPT 2002, Pasadena, CA (June 2002)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Hummel, J., Hendren, L.J., Nicolau, A.: A general data dependence test for dynamic, pointer-based data structures. In: Proc. ACM PLDI (1994)","DOI":"10.1145\/178243.178262"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM POPL (2001)","DOI":"10.1145\/360204.375719"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Muchnick, S.S.: Flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: Proc. 9th ACM POPL (1982)","DOI":"10.1145\/582153.582161"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-44674-5_15","volume-title":"Implementation and Application of Automata","author":"N. Klarlund","year":"2001","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, p. 182. Springer, Heidelberg (2001)"},{"key":"7_CR24","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. D. Van Nostrand Company, Inc., Princeton, New Jersey (1952); fifth reprint (1967)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-35767-X_24","volume-title":"Languages and Compilers for Parallel Computing","author":"V. Kuncak","year":"2003","unstructured":"Kuncak, V., Lam, P., Rinard, M.: A language for role specifications. In: Dietz, H.G. (ed.) LCPC 2001. LNCS, vol.\u00a02624, Springer, Heidelberg (2003)"},{"key":"7_CR26","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Roles are really great! Technical Report 822, Laboratory for Computer Science, Massachusetts Institute of Technology (2001)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. 29th POPL (2002)","DOI":"10.1145\/503272.503276"},{"key":"7_CR28","unstructured":"Kuncak, V., Rinard, M.: Typestate checking and regular graph constraints. Technical Report 863, MIT Laboratory for Computer Science (2002)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_24","volume-title":"Static Analysis","author":"V. Kuncak","year":"2003","unstructured":"Kuncak, V., Rinard, M.: Existential heap abstraction entailment is undecidable. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"7_CR30","unstructured":"Kuncak, V., Rinard, M.: On role logic. Technical Report 925, MIT CSAIL (2003)"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: On the boolean algebra of shape analysis constraints. Technical report, MIT CSAIL (August 2003)","DOI":"10.1007\/978-3-540-24622-0_7"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Larus, J.R., Hilfinger, P.N.: Detecting conflicts between structure accesses. In: Proc. ACM PLDI, Atlanta, GA (June 1988)","DOI":"10.1145\/53990.53993"},{"key":"7_CR33","unstructured":"Lev-Ami, T.: TVLA: A framework for kleene based logic static analyses. Master\u2019s thesis, Tel-Aviv University, Israel (2000)"},{"key":"7_CR34","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: International Symposium on Software Testing and Analysis (2000)","DOI":"10.1145\/347324.348031"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_3","volume-title":"Static Analysis","author":"F. Logozzo","year":"2003","unstructured":"Logozzo, F.: Class-level modular analysis for object oriented languages. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Manevich, R., Ramalingam, G., Field, J., Goyal, D., Sagiv, M.: Compactly representing first-order structures for static analysis. In: Proc. 9th International Static Analysis Symposium, pp. 196\u2013212 (2002)","DOI":"10.1007\/3-540-45789-5_16"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378851"},{"issue":"3","key":"7_CR38","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0020-0190(01)00155-7","volume":"80","author":"F. Nielson","year":"2001","unstructured":"Nielson, F., Nielson, H.R., Sagiv, M.: Kleene\u2019s logic with equality. Information Processing Letters\u00a080(3), 131\u2013137 (2001)","journal-title":"Information Processing Letters"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-36575-3_26","volume-title":"Programming Languages and Systems","author":"T. Reps","year":"2003","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 380\u2013398. Springer, Heidelberg (2003)"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. Technical Report TR-1468, University of Wisconsin (January 2003)","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"7_CR42","unstructured":"Rinetzky, N.: Interprocedural shape analysis. Master\u2019s thesis, Technion - Israel Institute of Technology (2000)"},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedual shape analysis for recursive programs. In: Proc. 10th International Conference on Compiler Construction (2001)","DOI":"10.1007\/3-540-45306-7_10"},{"issue":"1","key":"7_CR44","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 TOPLAS\u00a020(1), 1\u201350 (1998)","journal-title":"ACM TOPLAS"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proc. 26th ACM POPL (1999)","DOI":"10.1145\/292540.292552"},{"issue":"3","key":"7_CR46","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 TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"7_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, p. 366. Springer, Heidelberg (2000)"},{"key":"7_CR48","unstructured":"Yorsh, G.: Logical characterizations of heap abstractions. Master\u2019s thesis, Tel- Aviv University (March 2003)"},{"key":"7_CR49","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing mostprecise abstract operations for shape analysis. Technical report, Tel-Aviv University (September 2003) (forthcoming)","DOI":"10.1007\/978-3-540-24730-2_39"},{"key":"7_CR50","unstructured":"Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. Technical report, University of Wisconsin, Madison (January 2003)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T13:40:26Z","timestamp":1559569226000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}