{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T05:54:20Z","timestamp":1770270860062,"version":"3.49.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319127354","type":"print"},{"value":"9783319127361","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12736-1_24","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T14:53:24Z","timestamp":1413212004000},"page":"449-468","source":"Crossref","is-referenced-by-count":18,"title":["A Precise and Abstract Memory Model for C Using Symbolic Values"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[]},{"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Wilke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Bedin Fran\u00e7a, R., Blazy, S., Favre-Felix, D., Leroy, X., Pantel, M., Souyris, J.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS2 2012: Embedded Real Time Software and Systems (2012)"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Bernstein, D.J., Lange, T., Schwabe, P.: The Security Impact of a New Cryptographic Library. In: Hevia, A., Neven, G. (eds.) LATINCRYPT 2012. LNCS, vol.\u00a07533, pp. 159\u2013176. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-33481-8_9"},{"issue":"3","key":"24_CR3","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S. Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reasoning\u00a043(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"24_CR5","first-page":"85","volume":"254","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A Precise Yet Efficient Memory Model for C. ENTCS\u00a0254, 85\u2013103 (2009)","journal-title":"ENTCS"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103621.2103719"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-32347-8_8","volume-title":"Interactive Theorem Proving","author":"D. Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the Gap: Automatic Verified Abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 99\u2013115. Springer, Heidelberg (2012)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don\u2019t sweat the small stuff: Formal verification of C code without the pain. In: PLDI. ACM (2014)","DOI":"10.1145\/2594291.2594296"},{"key":"24_CR10","unstructured":"ISO. ISO C Standard 1999. Technical report (1999)"},{"key":"24_CR11","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.\u00a08307, pp. 50\u201365. Springer, Heidelberg (2013)"},{"key":"24_CR12","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. ACM (2014)","DOI":"10.1145\/2535838.2535878"},{"key":"24_CR13","unstructured":"Lee, D.: A memory allocator, http:\/\/gee.cs.oswego.edu\/dl\/html\/malloc.html"},{"issue":"7","key":"24_CR14","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. Comm. ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Comm. ACM"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Program Logics for Certified Compilers. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781107256552"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-34005-5_3","volume-title":"Rewriting Logic and Its Applications","author":"D. Lucanu","year":"2012","unstructured":"Lucanu, D., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: $\\mathbb{K}$ Framework Distilled. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol.\u00a07571, pp. 31\u201353. Springer, Heidelberg (2012)"},{"key":"24_CR17","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL, pp. 97\u2013108. ACM (2007)","DOI":"10.1145\/1190215.1190234"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Wang, X., Chen, H., Cheung, A., Jia, Z., Zeldovich, N., Kaashoek, M.F.: Undefined behavior: What happened to my code? In: APSYS 2012, pp. 1\u20137 (2012)","DOI":"10.1145\/2349896.2349905"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: Towards Optimization-safe Systems: Analyzing the Impact of Undefined Behavior. In: SOSP 2013, pp. 260\u2013275. ACM (2013)","DOI":"10.1145\/2517349.2522728"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12736-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T06:49:34Z","timestamp":1689576574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12736-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319127354","9783319127361"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12736-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}