{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:28:17Z","timestamp":1743118097986,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_10","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"150-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Separation Algebras for C Verification in Coq"],"prefix":"10.1007","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"volume-title":"Program Logics for Certified Compilers","year":"2014","key":"10_CR1","unstructured":"Appel, A.W. (ed.): Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-22863-6_5","volume-title":"Interactive Theorem Proving","author":"J Bengtson","year":"2011","unstructured":"Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying object-oriented programs with higher-order separation logic in Coq. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 22\u201338. Springer, Heidelberg (2011)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-54833-8_7","volume-title":"Programming Languages and Systems","author":"L Beringer","year":"2014","unstructured":"Beringer, L., Stewart, G., Dockins, R., Appel, A.W.: Verified compilation for shared-memory C. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 107\u2013127. Springer, Heidelberg (2014)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P. W., Parkinson, M. J.: Permission accounting in separation logic. In: POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P. W., Yangm, H.: Local action and abstract separation logic. In: LICS, pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"10_CR7","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual (2012)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-10672-9_13","volume-title":"Programming Languages and Systems","author":"R Dockins","year":"2009","unstructured":"Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 161\u2013177. Springer, Heidelberg (2009)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544 (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"10_CR10","unstructured":"International Organization for Standardization. ISO\/IEC 9899-2011: Programming languages - C. ISO Working Group 14 (2012)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-32347-8_22","volume-title":"Interactive Theorem Proving","author":"G Klein","year":"2012","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332\u2013337. Springer, Heidelberg (2012)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-03545-1_4","volume-title":"Certified Programs and Proofs","author":"R Krebbers","year":"2013","unstructured":"Krebbers, R.: Aliasing restrictions of C11 formalized in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 50\u201365. Springer, Heidelberg (2013)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. In: POPL, pp. 101\u2013112 (2014)","DOI":"10.1145\/2578855.2535878"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-642-22673-1_28","volume-title":"Intelligent Computer Mathematics","author":"R Krebbers","year":"2011","unstructured":"Krebbers, R., Wiedijk, F.: A  Formalization of the C99 Standard  in HOL, Isabelle and Coq. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 301\u2013303. Springer, Heidelberg (2011)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-37075-5_17","volume-title":"Foundations of Software Science and Computation Structures","author":"R Krebbers","year":"2013","unstructured":"Krebbers, R., Wiedijk, F.: Separation logic for non-local control flow and block scope variables. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 257\u2013272. Springer, Heidelberg (2013)"},{"issue":"7","key":"10_CR16","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107\u2013115 (2009)","journal-title":"CACM"},{"key":"10_CR17","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model, Version 2. Research report RR-7987, INRIA (2012)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-28644-8_4","volume-title":"CONCUR 2004 - Concurrency Theory","author":"PW O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49\u201367. Springer, Heidelberg (2004)"},{"key":"10_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":"PW 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. 2142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"issue":"1","key":"10_CR20","first-page":"41","volume":"2","author":"M Sozeau","year":"2010","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Formal Reasoning 2(1), 41\u201362 (2010)","journal-title":"J. Formal Reasoning"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T02:57:37Z","timestamp":1675997857000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}