{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:05:33Z","timestamp":1770275133418,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540474609","type":"print"},{"value":"9783540474623","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901433_22","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"400-419","source":"Crossref","is-referenced-by-count":31,"title":["Formal Verification of the Heap Manager of an Operating System Using Separation Logic"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Marti","sequence":"first","affiliation":[]},{"given":"Reynald","family":"Affeldt","sequence":"additional","affiliation":[]},{"given":"Akinori","family":"Yonezawa","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002). Invited lecture, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"22_CR2","unstructured":"Ruf, L., et al.: TOPSY \u2013 A Teachable Operating System, \n                    \n                      http:\/\/www.topsy.net\/"},{"key":"22_CR3","unstructured":"Ruf, L., Jeker, C., Lutz, B., Plattner, B.: Topsy v3: A NodeOS For Network Processors. In: 2nd International Workshop on Active Network Technologies and Applications (ANTA) (2003)"},{"key":"22_CR4","unstructured":"Various contributors. The Coq Proof assistant, \n                    \n                      http:\/\/coq.inria.fr"},{"key":"22_CR5","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Towards Formal Verification of Memory Properties using Separation Logic. In: 22nd Workshop of the Japan Society for Software Science and Technology, JSSST (2005)"},{"key":"22_CR6","unstructured":"Affeldt, R., Marti, N.: Towards Formal Verification of Memory Properties using Separation Logic. Online CVS, \n                    \n                      http:\/\/savannah.nongnu.org\/projects\/seplog"},{"issue":"1-3","key":"22_CR7","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.scico.2004.01.003","volume":"50","author":"D. Yu","year":"2004","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building Certified Libraries for PCC: Dynamic Storage Allocation. Science of Computer Programming\u00a050(1-3), 101\u2013127 (2004)","journal-title":"Science of Computer Programming"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-30124-0_21","volume-title":"Computer Science Logic","author":"T. Weber","year":"2004","unstructured":"Weber, T.: Towards Mechanized Program Verification with Separation Logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 250\u2013264. Springer, Heidelberg (2004)"},{"key":"22_CR9","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":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-32275-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Schirmer","year":"2005","unstructured":"Schirmer, N.: A Verification Environment for Sequential Imperative Programs in Isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 398\u2013414. Springer, Heidelberg (2005)"},{"key":"22_CR12","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F. Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving Pointer Programs in Higher-Order Logic. Information and Computation\u00a0199, 200\u2013227 (2005)","journal-title":"Information and Computation"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11591191_33","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Tuch","year":"2005","unstructured":"Tuch, H., Klein, G.: A Unified Memory Model for Pointers. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS, vol.\u00a03835, pp. 474\u2013488. Springer, Heidelberg (2005)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Hubert, T., March\u00e9, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005) (2005)","DOI":"10.1109\/SEFM.2005.1"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:37:04Z","timestamp":1619509024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11901433_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}