{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:01:18Z","timestamp":1765123278451},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540227915"},{"type":"electronic","value":"9783540278641"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27864-1_26","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T16:35:37Z","timestamp":1284654937000},"page":"361-376","source":"Crossref","is-referenced-by-count":7,"title":["Generalized Records and Spatial Conjunction in Role Logic"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"volume-title":"The Description Logic Handbook: Theory, Implementation and Applications","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)","key":"26_CR1"},{"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)","key":"26_CR2","DOI":"10.1145\/378795.378846"},{"key":"26_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":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-49099-X_2","volume-title":"Programming Languages and Systems","author":"M. Benedikt","year":"1999","unstructured":"Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, p. 2. Springer, Heidelberg (1999)"},{"key":"26_CR5","first-page":"220","volume-title":"31st ACM POPL","author":"L. Birkedal","year":"2004","unstructured":"Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: 31st ACM POPL, pp. 220\u2013231. ACM Press, New York (2004)"},{"doi-asserted-by":"crossref","unstructured":"Calcagno, C., Cardelli, L., Gordon, A.D.: Deciding validity in a spatial logic for trees. In: ACM TLDI 2002 (2002)","key":"26_CR6","DOI":"10.1145\/604174.604183"},{"key":"26_CR7","volume-title":"Theoretical Aspects of Object-Oriented Programming","author":"L. Cardelli","year":"1994","unstructured":"Cardelli, L., Mitchell, J.C.: Operations on records. In: Theoretical Aspects of Object-Oriented Programming, The MIT Press, Cambridge (1994)"},{"doi-asserted-by":"crossref","unstructured":"Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: Proc. ACM PLDI (1990)","key":"26_CR8","DOI":"10.1145\/93542.93585"},{"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: Proc. 4th POPL (1977)","key":"26_CR9","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA 2003 (2003)","key":"26_CR10","DOI":"10.1145\/949305.949332"},{"doi-asserted-by":"crossref","unstructured":"Fradet, P., M\u00e9tayer, D.L.: Shape types. In: Proc. 24th ACM POPL (1997)","key":"26_CR11","DOI":"10.1145\/263699.263706"},{"unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS 1997, Warschau (1997)","key":"26_CR12"},{"doi-asserted-by":"crossref","unstructured":"Harper, R., Pierce, B.: A record calculus based on symmetric concatenation. In: 18th ACM POPL, Orlando, Florida, pp. 131\u2013142 (1991)","key":"26_CR13","DOI":"10.1145\/99583.99603"},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: 31st POPL (2004)","key":"26_CR14","DOI":"10.1145\/964001.964021"},{"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)","key":"26_CR15","DOI":"10.1145\/178243.178262"},{"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)","key":"26_CR16","DOI":"10.1145\/360204.375719"},{"unstructured":"Jones, M., Jones, S.P.: Lightweight extensible records for Haskell. In: Haskell Workshop (1999)","key":"26_CR17"},{"unstructured":"Kuncak, V.: Designing an algorithm for role analysis. Master\u2019s thesis, MIT Laboratory for Computer Science (2001)","key":"26_CR18"},{"doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. 29th POPL (2002)","key":"26_CR19","DOI":"10.1145\/503272.503276"},{"unstructured":"Kuncak, V., Rinard, M.: Typestate checking and regular graph constraints. Technical Report 863, MIT Laboratory for Computer Science (2002)","key":"26_CR20"},{"key":"26_CR21","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)"},{"unstructured":"Kuncak, V., Rinard, M.: On role logic. Technical Report 925, MIT CSAIL (2003)","key":"26_CR22"},{"doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: On the boolean algebra of shape analysis constraints. Technical report, MIT CSAIL (August 2003)","key":"26_CR23","DOI":"10.1007\/978-3-540-24622-0_7"},{"doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Boolean algebra of shape analysis constraints. In: Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation (2004)","key":"26_CR24","DOI":"10.1007\/978-3-540-24622-0_7"},{"doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: On generalized records and spatial conjunction in role logic. Technical Report 942, MIT CSAIL (April 2004)","key":"26_CR25","DOI":"10.1007\/978-3-540-27864-1_26"},{"unstructured":"Lam, P., Kuncak, V., Rinard, M.: On modular pluggable analyses using set interfaces. Technical Report 933, MIT CSAIL (December 2003)","key":"26_CR26"},{"key":"26_CR27","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/981009.981016","volume":"39","author":"P. Lam","year":"2004","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Notices\u00a039, 46\u201355 (2004)","journal-title":"SIGPLAN Notices"},{"doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM PLDI (2001)","key":"26_CR28","DOI":"10.1145\/378795.378851"},{"key":"26_CR29","series-title":"Lecture Notes in Logic","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-21676-7","volume-title":"Bounded Variable Logics and Counting: A Study in Finite Models","author":"M. Otto","year":"1997","unstructured":"Otto, M.: Bounded Variable Logics and Counting: A Study in Finite Models. Lecture Notes in Logic, vol.\u00a09. Springer, Heidelberg (1997)"},{"issue":"4","key":"26_CR30","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1137\/S0097539797323005","volume":"29","author":"L. Pacholski","year":"2000","unstructured":"Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first-order twovariable logic with counting. SIAM J. on Computing\u00a029(4), 1083\u20131117 (2000)","journal-title":"SIAM J. on Computing"},{"doi-asserted-by":"crossref","unstructured":"Pottier, F.: A constraint-based presentation and generalization of rows. In: 18th IEEE LICS (June 2003)","key":"26_CR31","DOI":"10.1109\/LICS.2003.1210073"},{"doi-asserted-by":"crossref","unstructured":"Remy, D.: Typing record concatenation for free. In: POPL, pp. 166\u2013176 (1992)","key":"26_CR32","DOI":"10.1145\/143165.143202"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th LICS, pp. 55\u201374 (2002)","key":"26_CR33","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"26_CR34","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"},{"doi-asserted-by":"crossref","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE TSE (January 1986)","key":"26_CR35","DOI":"10.1109\/TSE.1986.6312929"},{"issue":"1","key":"26_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90050-C","volume":"93","author":"M. Wand","year":"1991","unstructured":"Wand, M.: Type inference for record concatenation and multiple inheritance. Information and Computation\u00a093(1), 1\u201315 (1991)","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: PLDI (2004)","key":"26_CR37","DOI":"10.1145\/996841.996846"},{"unstructured":"Yorsh, G.: Logical characterizations of heap abstractions. Master\u2019s thesis, Tel-Aviv University (March 2003)","key":"26_CR38"},{"key":"26_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27864-1_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:24:43Z","timestamp":1605759883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27864-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540227915","9783540278641"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27864-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}