{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T08:12:55Z","timestamp":1791187975369,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642323461","type":"print"},{"value":"9783642323478","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_8","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T11:33:54Z","timestamp":1344598434000},"page":"99-115","source":"Crossref","is-referenced-by-count":43,"title":["Bridging the Gap: Automatic Verified Abstraction of C"],"prefix":"10.1007","author":[{"given":"David","family":"Greenaway","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2-4","key":"8_CR1","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s10817-009-9123-z","volume":"42","author":"E. Alkassar","year":"2009","unstructured":"Alkassar, E., Hillebrand, M., Leinenbach, D., Schirmer, N., Starostin, A., Tsyban, A.: Balancing the load \u2014 leveraging a semantics stack for systems verification. JAR: Special Issue Operat. Syst.\u00a042(2-4), 389\u2013454 (2009)","journal-title":"JAR: Special Issue Operat. Syst."},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15057-9_5","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Paul, W.J., Starostin, A., Tsyban, A.: Pervasive Verification of an OS Microkernel. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 71\u201385. Springer, Heidelberg (2010)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure Microkernels, State Monads and Scalable Refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"8_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":"8_CR5","unstructured":"The Frama-C platform (2008), http:\/\/www.frama-c.cea.fr\/"},{"key":"8_CR6","unstructured":"ISO\/IEC. Programming languages \u2014 C. Technical Report 9899:TC2, ISO\/IEC JTC1\/SC22\/WG14 (May 2005)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: 22nd SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"8_CR8","unstructured":"Moy, Y.: Automatic Modular Static Safety Checking for C Programs. PhD thesis, Universit\u00e9 Paris-Sud, Paris, France (January 2009)"},{"key":"8_CR9","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers (1997)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"8_CR11","unstructured":"Norrish, M.: C-to-Isabelle parser, version 0.7.2 (January 2012), http:\/\/ertos.nicta.com.au\/software\/c-parser\/"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"8_CR13","unstructured":"Tuch, H.: Formal Memory Models for Verifying C Systems Code. PhD thesis, School Comp. Sci. & Engin., University NSW, Sydney 2052, Australia (August 2008)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) 34th POPL, pp. 97\u2013108. ACM (2007)","DOI":"10.1145\/1190216.1190234"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-03359-9_34","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Winwood","year":"2009","unstructured":"Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., Norrish, M.: Mind the Gap: A Verification Framework for Low-Level C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 500\u2013515. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32347-8_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:09:47Z","timestamp":1606187387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}