{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:28Z","timestamp":1772164048742,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,6,16]],"date-time":"2013-06-16T00:00:00Z","timestamp":1371340800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,6,16]]},"DOI":"10.1145\/2491956.2462183","type":"proceedings-article","created":{"date-parts":[[2013,6,11]],"date-time":"2013-06-11T12:03:50Z","timestamp":1370952230000},"page":"471-482","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":91,"title":["Translation validation for a verified OS kernel"],"prefix":"10.1145","author":[{"given":"Thomas Arthur Leck","family":"Sewell","sequence":"first","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"Cambridge University, Cambridge, United Kingdom"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}]}],"member":"320","published-online":{"date-parts":[[2013,6,16]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"LNCS","first-page":"71","volume-title":"P. O'Hearn","author":"Alkassar E.","year":"2010","unstructured":"E. Alkassar , W. Paul , A. Starostin , and A. Tsyban . Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices . In P. O'Hearn , G. T. Leavens, and S. Rajamani, editors, VSTTE 2010 , volume 6217 of LNCS , pages 71 -- 85 , Edinburgh, UK, Aug 2010. Springer . E. Alkassar, W. Paul, A. Starostin, and A. Tsyban. Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In P. O'Hearn, G. T. Leavens, and S. Rajamani, editors, VSTTE 2010, volume 6217 of LNCS, pages 71--85, Edinburgh, UK, Aug 2010. Springer."},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"1","volume-title":"Proc. 20th ESOP","author":"Appel A. W.","year":"2011","unstructured":"A. W. Appel . Verified software toolchain?(invited talk) . In G. Barthe, editor, Proc. 20th ESOP , volume 6602 of LNCS , pages 1 -- 17 , Saarbr\u00fccken, Germany, Mar . 2011 . Springer . A. W. Appel. Verified software toolchain?(invited talk). In G. Barthe, editor, Proc. 20th ESOP, volume 6602 of LNCS, pages 1--17, Saarbr\u00fccken, Germany, Mar. 2011. Springer."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1785141.1785156"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"L. M.\n      de Moura\n     and \n      N.\n      Bj\u00f8rner\n  . \n  Z3: An efficient SMT solver\n  . In C. R. Ramakrishnan and J. Rehof editors 14th TACAS volume \n  4963\n   of \n  LNCS pages \n  337\n  --\n  340 Budapest Hungary Mar. \n  2008\n  . \n  Springer\n  .   L. M. de Moura and N. Bj\u00f8rner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and J. Rehof editors 14th TACAS volume 4963 of LNCS pages 337--340 Budapest Hungary Mar. 2008. Springer.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.030"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2010.2042889"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_16_1","volume-title":"University of Cambridge","author":"Myreen M. O.","year":"2009","unstructured":"M. O. Myreen . Formal verification of machine-code programs. PhD thesis , University of Cambridge , 2009 . M. O. Myreen. Formal verification of machine-code programs. PhD thesis, University of Cambridge, 2009."},{"key":"e_1_3_2_1_17_1","first-page":"1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Myreen M. O.","year":"2008","unstructured":"M. O. Myreen , M. J. C. Gordon , and K. Slind . Machine-code verification for multiple architectures - an application of decompilation into logic . In A. Cimatti and R. B. Jones, editors, Formal Methods in Computer-Aided Design (FMCAD) , pages 1 -- 8 . IEEE , 2008 . M. O. Myreen, M. J. C. Gordon, and K. Slind. Machine-code verification for multiple architectures - an application of decompilation into logic. In A. Cimatti and R. B. Jones, editors, Formal Methods in Computer-Aided Design (FMCAD), pages 1--8. IEEE, 2008."},{"key":"e_1_3_2_1_18_1","first-page":"78","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Myreen M. O.","year":"2012","unstructured":"M. O. Myreen , M. J. C. Gordon , and K. Slind . Decompilation into logic -- improved . In G. Cabodi and S. Singh, editors, Formal Methods in Computer-Aided Design (FMCAD) , pages 78 -- 81 . IEEE , 2012 . M. O. Myreen, M. J. C. Gordon, and K. Slind. Decompilation into logic -- improved. In G. Cabodi and S. Singh, editors, Formal Methods in Computer-Aided Design (FMCAD), pages 78--81. IEEE, 2012."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_20_1","series-title":"LNCS","first-page":"189","volume-title":"Proc. 20th TPHOLs","author":"Ni Z.","year":"2007","unstructured":"Z. Ni , D. Yu , and Z. Shao . Using XCAP to certify realistic systems code: machine context management . In Proc. 20th TPHOLs , volume 4732 of LNCS , pages 189 -- 206 . Springer , 2007 . Z. Ni, D. Yu, and Z. Shao. Using XCAP to certify realistic systems code: machine context management. In Proc. 20th TPHOLs, volume 4732 of LNCS, pages 189--206. Springer, 2007."},{"key":"e_1_3_2_1_21_1","series-title":"LNCS","volume-title":"Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer , 2002 . T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002."},{"key":"e_1_3_2_1_22_1","unstructured":"Open Kernel Labs. seL4 research and evaluation download. http:\/\/ertos.nicta.com.au\/software\/seL4\/ 2011.  Open Kernel Labs. seL4 research and evaluation download. http:\/\/ertos.nicta.com.au\/software\/seL4\/ 2011."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986333"},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","first-page":"151","volume-title":"Proc. 4th TACAS","author":"Pnueli A.","year":"1998","unstructured":"A. Pnueli , M. Siegel , and E. Singerman . Translation validation . In B. Steffen, editor, Proc. 4th TACAS , volume 1384 of LNCS , pages 151 -- 166 . Springer , 1998 . A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In B. Steffen, editor, Proc. 4th TACAS, volume 1384 of LNCS, pages 151--166. Springer, 1998."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_57"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"T.\n      Sewell S.\n      Winwood P.\n      Gammie T.\n      Murray J.\n      Andronick and \n      G.\n      Klein\n  . \n  seL4 enforces integrity\n  . In M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk editors 2nd Int. Conf. on Interactive Theorem Proving volume \n  6898\n   of \n  LNCS pages \n  325\n  --\n  340 Nijmegen The Netherlands Aug. \n  2011\n  . \n  Springer\n  .   T. Sewell S. Winwood P. Gammie T. Murray J. Andronick and G. Klein. seL4 enforces integrity. In M. C. J. D. van Eekelen H. Geuvers J. Schmaltz and F. Wiedijk editors 2nd Int. Conf. on Interactive Theorem Proving volume 6898 of LNCS pages 325--340 Nijmegen The Netherlands Aug. 2011. Springer.","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9120-2"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80584-X"},{"issue":"3","key":"e_1_3_2_1_36_1","first-page":"223","article-title":"VOC: A methodology for the translation validation of optimizing compilers","volume":"9","author":"Zuck L. D.","year":"2003","unstructured":"L. D. Zuck , A. Pnueli , and B. Goldberg . VOC: A methodology for the translation validation of optimizing compilers . J. UCS , 9 ( 3 ): 223 -- 247 , 2003 . L. D. Zuck, A. Pnueli, and B. Goldberg. VOC: A methodology for the translation validation of optimizing compilers. J. UCS, 9(3):223--247, 2003.","journal-title":"J. UCS"}],"event":{"name":"PLDI '13: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Seattle Washington USA","acronym":"PLDI '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2462183","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491956.2462183","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:28:41Z","timestamp":1750217321000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2462183"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,16]]},"references-count":34,"alternative-id":["10.1145\/2491956.2462183","10.1145\/2491956"],"URL":"https:\/\/doi.org\/10.1145\/2491956.2462183","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2499370.2462183","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,6,16]]},"assertion":[{"value":"2013-06-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}