{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T04:13:51Z","timestamp":1744172031902,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642333132"},{"type":"electronic","value":"9783642333149"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33314-9_1","type":"book-chapter","created":{"date-parts":[[2012,9,12]],"date-time":"2012-09-12T04:05:18Z","timestamp":1347422718000},"page":"1-16","source":"Crossref","is-referenced-by-count":1,"title":["Transitive Separation Logic"],"prefix":"10.1007","author":[{"given":"Han-Hing","family":"Dang","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"M\u00f6ller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local Action and Abstract Separation Logic. In: Proc. of the 22nd Symposium on Logic in Computer Science, pp. 366\u2013378. IEEE Press (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-13321-3_7","volume-title":"Mathematics of Program Construction","author":"Y. Chen","year":"2010","unstructured":"Chen, Y., Sanders, J.W.: Abstraction of Object Graphs in Program Verification. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol.\u00a06120, pp. 80\u201399. Springer, Heidelberg (2010)"},{"issue":"6","key":"1_CR4","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.jlap.2011.04.003","volume":"80","author":"H.H. Dang","year":"2011","unstructured":"Dang, H.H., H\u00f6fner, P., M\u00f6ller, B.: Algebraic separation logic. Journal of Logic and Algebraic Programming\u00a080(6), 221\u2013247 (2011)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0020-0255(01)00168-2","volume":"139","author":"J. Desharnais","year":"2001","unstructured":"Desharnais, J., M\u00f6ller, B.: Characterizing determinacy in Kleene algebra. Information Sciences\u00a0139, 253\u2013273 (2001)","journal-title":"Information Sciences"},{"issue":"4","key":"1_CR6","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J. Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic\u00a07(4), 798\u2013833 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"key":"1_CR7","unstructured":"Ehm, T.: The Kleene algebra of nested pointer structures: Theory and applications, PhD Thesis (2003), http:\/\/www.opus-bayern.de\/uni-augsburg\/frontdoor.php?source_opus=89"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-24771-5_9","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"T. Ehm","year":"2004","unstructured":"Ehm, T.: Pointer Kleene Algebra. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS\/Kleene-Algebra Ws 2003. LNCS, vol.\u00a03051, pp. 99\u2013111. Springer, Heidelberg (2004)"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proofs of correctness of data representations. Acta Informatica\u00a01, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-23217-6_17","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"C.A.R. Hoare","year":"2011","unstructured":"Hoare, C.A.R., Hussain, A., M\u00f6ller, B., O\u2019Hearn, P.W., Petersen, R.L., Struth, G.: On Locality and the Exchange Law for Concurrent Processes. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 250\u2013264. Springer, Heidelberg (2011)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"H\u00f6fner, P., Struth, G.: Can refinement be automated? In: Boiten, E., Derrick, J., Smith, G. (eds.) Refine 2007. ENTCS, vol.\u00a0201, pp. 197\u2013222. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.02.021"},{"issue":"2","key":"1_CR12","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation\u00a0110(2), 366\u2013390 (1994)","journal-title":"Information and Computation"},{"issue":"3","key":"1_CR13","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems\u00a019(3), 427\u2013443 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BF02572645","volume":"31","author":"E. Manes","year":"1985","unstructured":"Manes, E., Benson, D.: The inverse semigroup of a sum-ordered semiring. Semigroup Forum\u00a031, 129\u2013152 (1985)","journal-title":"Semigroup Forum"},{"key":"1_CR15","unstructured":"McCune, W.W.: Prover9 and Mace4, http:\/\/www.cs.unm.edu\/~mccune\/prover9"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"M\u00f6ller, B.: Some applications of pointer algebra. In: Broy, M. (ed.) Programming and Mathematical Method. NATO ASI Series, Series F: Computer and Systems Sciences, vol.\u00a088, pp. 123\u2013155. Springer (1992)","DOI":"10.1007\/978-3-642-77572-7_8"},{"issue":"3-4","key":"1_CR17","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0020-0255(99)00011-0","volume":"119","author":"B. M\u00f6ller","year":"1999","unstructured":"M\u00f6ller, B.: Calculating with acyclic and cyclic lists. Information Sciences\u00a0119(3-4), 135\u2013154 (1999)","journal-title":"Information Sciences"},{"issue":"1-3","key":"1_CR18","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, Concurrency, and Local Reasoning. Theoretical Computer Science\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: An introduction to separation logic. In: Broy, M. (ed.) Engineering Methods and Tools for Software Safety and Security, pp. 285\u2013310. IOS Press (2009)","DOI":"10.3233\/978-1-58603-976-9-285"},{"issue":"2","key":"1_CR20","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.tcs.2005.09.071","volume":"351","author":"E.J. Sims","year":"2006","unstructured":"Sims, E.J.: Extending Separation Logic with Fixpoints and Postponed Substitution. Theoretical Computer Science\u00a0351(2), 258\u2013275 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Wang, S., Barbosa, L.S., Oliveira, J.N.: A Relational Model for Confined Separation Logic. In: Proc. of the 2nd IFIP\/IEEE Intl. Symposium on Theoretical Aspects of Software Engineering, TASE 2008, pp. 263\u2013270. IEEE Press (2008)","DOI":"10.1109\/TASE.2008.38"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33314-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T08:58:01Z","timestamp":1744102681000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33314-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642333132","9783642333149"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33314-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}