{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:11:18Z","timestamp":1770279078823,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540227915","type":"print"},{"value":"9783540278641","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27864-1_25","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T12:35:37Z","timestamp":1284640537000},"page":"344-360","source":"Crossref","is-referenced-by-count":11,"title":["On Logics of Aliasing"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","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 describing linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 2\u201319. Springer, Heidelberg (1999)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Storeless Semantics and Alias Logic. In: Proc. ACM SIGPLAN 2003 Workshop on Partial Evaluation and Semantics Based Program Manipulation, pp. 55\u201365 (2003)","DOI":"10.1145\/777388.777395"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: On Logics of Aliasing. Technical Report TR-2004-4, VERIMAG, http:\/\/www-verimag.imag.fr\/~iosif\/TR-2004-4.ps","DOI":"10.1007\/978-3-540-27864-1_25"},{"key":"25_CR4","unstructured":"Bozga, M., Iosif, R.: On Model Checking Generic Topologies. Technical Report TR- 2004-10, VERIMAG, http:\/\/www-verimag.imag.fr\/~iosif\/TR-2004-10.ps"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C. Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Cardelli, L., Gordon, A.: Deciding Validity in a Spatial Logic of Trees. In: ACM Workshop on Types in Language Design and Implementation, pp. 62\u201373 (2003)","DOI":"10.1145\/604174.604183"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Courcelle, B.: Handbook of graph grammars and computing by graph transformations. In: The expression of graph properties and graph transformations in monadic second-order logic: Foundations, vol.\u00a01, ch. 5, pp. 313\u2013400 (1997)","DOI":"10.1142\/9789812384720_0005"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Deutsch, A.: A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations. In: Proceedings of the IEEE 1992 Conference on Computer Languages, pp. 2\u201313 (1992)","DOI":"10.1109\/ICCL.1992.185463"},{"key":"25_CR9","volume-title":"Finite Model Theory","author":"H.D. Ebbinghaus","year":"1999","unstructured":"Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1999)"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Proc. Symposium on Applied Mathematics. American Mathematical Society, vol.\u00a01, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Galmiche, D., Mery, D.: Semantic Labelled Tableaux for propositional BI (without bottom). Journal of Logic and Computation 13(5) (2003)","DOI":"10.1093\/logcom\/13.5.707"},{"key":"25_CR12","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, pp. 1\u201318. Springer, Heidelberg (1999)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an Assertion Language for Mutable Data Structures. In: Proc. of 28th ACM-SIGPLAN Symposium on Principles of Programming Languages (2001)","DOI":"10.1145\/360204.375719"},{"key":"25_CR14","series-title":"Algorithmic Languages","first-page":"321","volume-title":"Abstract Storage Structures","author":"H.B.M. Jonkers","year":"1981","unstructured":"Jonkers, H.B.M.: Abstract Storage Structures. Algorithmic Languages, pp. 321\u2013343. North-Holland, Amsterdam (1981)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0017482","volume-title":"Trees in Algebra and Programming - CAAP \u201994","author":"N. Klarlund","year":"1994","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graphs and Decidable Transductions Based on Edge Constraints. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 187\u2013201. Springer, Heidelberg (1994)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph Types. In: Proc. 20th Annual Symposium on Principles of Programming Languages, pp. 196\u2013205 (1993)","DOI":"10.1145\/158511.158628"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Moeller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM SIGPLAN Conference on Programming Languages Design and Implementation (2001)","DOI":"10.1145\/378795.378851"},{"issue":"2","key":"25_CR18","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The Logic of Bunched Implications. Bulletin of Symbolic Logic\u00a05(2), 215\u2013244 (1999)","journal-title":"Bulletin of Symbolic Logic"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. Amer. Math. Soc.\u00a0141 (1969)","DOI":"10.2307\/1995086"},{"issue":"5","key":"25_CR21","doi-asserted-by":"publisher","first-page":"1467","DOI":"10.1145\/186025.186041","volume":"16","author":"G. Ramalingam","year":"1994","unstructured":"Ramalingam, G.: The Undecidability of Aliasing. ACM Transactions on Programming Languages and Systems\u00a016(5), 1467\u20131471 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proc 17th IEEE Symposium on Logic in Computer Science (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"25_CR23","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, M.T., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. ACM Transactions on Programming Languages and Systems\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"25_CR24","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1993","unstructured":"Smullyan, R.M.: First-Order Logic. Dover Publications, New York (1993)"},{"key":"25_CR25","volume-title":"Logic and Structure","author":"D. Dalen van","year":"1997","unstructured":"van Dalen, D.: Logic and Structure. Springer, Heidelberg (1997)"}],"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_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:24:43Z","timestamp":1605741883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27864-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540227915","9783540278641"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27864-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}