{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:38:45Z","timestamp":1725633525596},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642353079"},{"type":"electronic","value":"9783642353086"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_7","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"43-59","source":"Crossref","is-referenced-by-count":3,"title":["On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor"],"prefix":"10.1007","author":[{"given":"Dominic P.","family":"Mulligan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A. Asperti","year":"2007","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Automated Reasoning\u00a039, 109\u2013139 (2007)","journal-title":"Automated Reasoning"},{"key":"7_CR2","unstructured":"Boender, J., Sacerdoti Coen, C.: On the correctness of a branch displacement algorithm (2012), \n                  \n                    http:\/\/arxiv.org\/abs\/1209.5920"},{"key":"7_CR3","unstructured":"The CerCo FET-Open project (2011), \n                  \n                    http:\/\/cerco.cs.unibo.it\/"},{"key":"7_CR4","unstructured":"Branch displacement optimisation (2006), \n                  \n                    http:\/\/groups.google.com\/group\/alt.lang.asm\/msg\/d31192d442accad3"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an operating system kernel. In: SOSP (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"4","key":"7_CR6","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Transactions on Programming Languages and Systems\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"7_CR7","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Automated Reasoning"},{"key":"7_CR8","unstructured":"Moore, J.S.: Piton: A mechanically verified assembly language. Automated Reasoning Series, vol.\u00a03. Springer (1996)"},{"key":"7_CR9","unstructured":"Moore, J.S.: A grand challenge proposal for formal methods (2005)"},{"key":"7_CR10","unstructured":"Small device C compiler 3.0.0 (2011), \n                  \n                    http:\/\/sdcc.sourceforge.net\/"},{"key":"7_CR11","unstructured":"Siemens Semiconductor Group 8051 derivative instruction set (2011), \n                  \n                    http:\/\/www.win.tue.nl\/~aeb\/comp\/8051\/instruction-set.pdf"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset Coercions in Coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL, pp. 97\u2013108 (2007)","DOI":"10.1145\/1190215.1190234"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. In: POPL, pp. 43\u201354 (2011)","DOI":"10.1145\/1925844.1926393"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:13:51Z","timestamp":1620134031000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}