{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:58:17Z","timestamp":1762865897321,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642277047"},{"type":"electronic","value":"9783642277054"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_3","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T12:18:06Z","timestamp":1327493886000},"page":"18-33","source":"Crossref","is-referenced-by-count":5,"title":["Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT"],"prefix":"10.1007","author":[{"given":"Sabine","family":"Schmaltz","sequence":"first","affiliation":[]},{"given":"Andrey","family":"Shadrin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP)","author":"G. Klein","year":"2009","unstructured":"Klein, G., et al.: seL4: Formal verification of an OS kernel. In: Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220. ACM, Big Sky (2009)"},{"key":"3_CR2","first-page":"97","volume-title":"POPL 2007: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"H. Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL 2007: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97\u2013108. ACM, New York (2007)"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/1111037.1111066","volume-title":"POPL 2006: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Z. Ni","year":"2006","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL 2006: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 320\u2013333. ACM, New York (2006)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-74591-4_15","volume-title":"Theorem Proving in Higher Order Logics","author":"Z. Ni","year":"2007","unstructured":"Ni, Z., Yu, D., Shao, Z.: Using XCAP to Certify Realistic Systems Code: Machine Context Management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 189\u2013206. Springer, Heidelberg (2007)"},{"issue":"2-4","key":"3_CR5","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10817-009-9118-9","volume":"42","author":"X. Feng","year":"2009","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reasoning\u00a042(2-4), 301\u2013347 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Leinenbach, D., Petrova, E.: Pervasive compiler verification \u2013 from verified programs to verified systems. In: 3rd Intl Workshop on Systems Software Verification (SSV 2008). Elsevier Science B. V. (2008)","DOI":"10.1016\/j.entcs.2008.06.040"},{"issue":"3","key":"3_CR7","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. Journal of Automated Reasoning\u00a043(3), 263\u2013288 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"7","key":"3_CR8","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. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"A.W. Appel","year":"2011","unstructured":"Appel, A.W.: Verified Software Toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 1\u201317. Springer, Heidelberg (2011)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Types in Compilation","author":"J.G. Morrisett","year":"1998","unstructured":"Morrisett, J.G., Crary, K., Glew, N., Walker, D.: Stack-Based Typed Assembly Language. In: Leroy, X., Ohori, A. (eds.) TIC 1998. LNCS, vol.\u00a01473, pp. 28\u201352. Springer, Heidelberg (1998)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-56992-8_17","volume-title":"Computer Science Logic","author":"Y. Gurevich","year":"1993","unstructured":"Gurevich, Y., Huggins, J.K.: The Semantics of the C Programming Language. In: Martini, S., B\u00f6rger, E., Kleine B\u00fcning, H., J\u00e4ger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol.\u00a0702, pp. 274\u2013308. Springer, Heidelberg (1993)"},{"key":"3_CR12","unstructured":"Papaspyrou, N.S.: A formal semantics for the C programming language. tech. report (1998)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-540-79980-1_22","volume-title":"Algebraic Methodology and Software Technology","author":"S. Maus","year":"2008","unstructured":"Maus, S., Moska\u0142, M., Schulte, W.: Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving. In: Bevilacqua, V., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol.\u00a05140, pp. 284\u2013298. Springer, Heidelberg (2008)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Hillebrand, M.A., Paul, W., Petrova, E.: Automated Verification of a Small Hypervisor. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 40\u201354. Springer, Heidelberg (2010)"},{"key":"3_CR15","unstructured":"Cohen, E., Schirmer, N.: A better reduction theorem for store buffers. CoRR abs\/0909.4637 (2009)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T12:29:30Z","timestamp":1556195370000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}