{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:02:32Z","timestamp":1767999752728,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540230243","type":"print"},{"value":"9783540301240","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_21","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T17:27:59Z","timestamp":1267550879000},"page":"250-264","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Towards Mechanized Program Verification with Separation Logic"],"prefix":"10.1007","author":[{"given":"Tjark","family":"Weber","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"issue":"4","key":"21_CR1","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"R. Krzysztof","year":"1981","unstructured":"Krzysztof, R.: Apt. Ten years of Hoare\u2019s logic: A survey \u2013 part I. ACM Transactions on Programming Languages and Systems\u00a03(4), 431\u2013483 (1981)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"21_CR2","first-page":"83","volume":"28","author":"R. Krzysztof","year":"1984","unstructured":"Krzysztof, R.: Apt. Ten years of Hoare\u2019s logic: A survey \u2013 part II: Nondeterminism. Theoretical Computer Science\u00a028, 83\u2013109 (1984)","journal-title":"Theoretical Computer Science"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C.W. Barrett","year":"1996","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"21_CR4","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1145\/964001.964020","volume-title":"Proceedings of the 31-st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"L. Birkedal","year":"2004","unstructured":"Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: Proceedings of the 31-st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 220\u2013231. ACM Press, New York (2004)"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. Mathematics of Program Construction, 102\u2013126 (2000)","DOI":"10.1007\/10722010_8"},{"key":"21_CR6","first-page":"23","volume-title":"Machine Intelligence","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a07, pp. 23\u201350. Edinburgh University Press, Edinburgh (1972)"},{"key":"21_CR7","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":"21_CR8","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. Dijkstra","year":"1975","unstructured":"Dijkstra, E.: Guarded commands, non-determinacy and formal derivation of programs. Communications of the ACM\u00a018, 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"issue":"10","key":"21_CR9","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"21_CR10","volume-title":"The C Programming Language","author":"B.W. Kernighan","year":"1988","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice Hall, Englewood Cliffs (1988)","edition":"2"},{"key":"21_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction \u2013 CADE-19","author":"F. Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"issue":"2","key":"21_CR12","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing\u00a010(2), 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-94-010-0413-8_11","volume-title":"Proof and System-Reliability","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"21_CR15","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":"21_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 305\u2013320. Springer, Heidelberg (2004)"},{"key":"21_CR18","unstructured":"Yang, H.: Local Reasoning for Stateful Programs. PhD thesis, University of Illinois, Urbana-Champaign (2001)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Yang, H., O\u2019Hearn, P.W.: A semantic basis for local reasoning. In: Foundations of Software Science and Computation Structure, pp. 402\u2013416 (2002)","DOI":"10.1007\/3-540-45931-6_28"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T23:00:55Z","timestamp":1739919655000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}