{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T02:07:21Z","timestamp":1746324441923,"version":"3.28.0"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894252","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T04:25:06Z","timestamp":1573619106000},"page":"1-9","source":"Crossref","is-referenced-by-count":2,"title":["Scalable Translation Validation of Unverified Legacy OS Code"],"prefix":"10.23919","author":[{"given":"Amer","family":"Tahat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarang","family":"Joshi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pronnoy","family":"Goswami","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75698-9_18"},{"key":"ref32","first-page":"118","article-title":"Towards Rigorous Compiler Implementation Verification","author":"goerigk","year":"1997","journal-title":"Proc of the 1997 Workshop on Programming Languages and Fundamentals of Programming"},{"key":"ref31","first-page":"151","article-title":"Translation validation","author":"pnueli","year":"1998","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628143"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837615"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","article-title":"A trustworthy monadic formalization of the armv7 instruction set architecture","author":"fox","year":"2010","journal-title":"Interactive Theorem Proving First International Conference ITP 2010 Edinburgh UK July 11-14 2010 Proceedings"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_12"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"ref15","first-page":"41","author":"alglave","year":"2011","journal-title":"Litmus Running Tests against Hardware"},{"journal-title":"Radare2","year":"2018","author":"alvarez","key":"ref16"},{"journal-title":"The PVS Proof Checker A Reference Manual","year":"1993","author":"shankar","key":"ref17"},{"key":"ref18","first-page":"42","article-title":"End-to-end verification of processors with isa-formal","author":"reid","year":"2016","journal-title":"Computer Aided Verification-28th International Conference CAV 2016 Toronto ON Canada July 17-23 2016 Proceedings Part II"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"ref28","volume":"1254","author":"grumberg","year":"1997","journal-title":"Computer Aided Verification 9th International Conference CAV ’97 Haifa Israel June 22-25 1997 Proceedings"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"ref27","first-page":"151","article-title":"Translation validation","author":"pnueli","year":"1998","journal-title":"Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_1"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2016.7461326"},{"key":"ref8","first-page":"22:1","article-title":"Compcerttso: A verified compiler for relaxed-memory concurrency","volume":"60","author":"\u0161ev?\u00edk","year":"2013","journal-title":"J ACM"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48257-1_24"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2893177"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"journal-title":"Unicorn-The ultimate CPU emulator","year":"2018","author":"quynh","key":"ref20"},{"journal-title":"ARM v8 Manual","year":"2019","key":"ref22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"ref24","article-title":"Batch proving and proof scripting in PVS","author":"munoz","year":"2007","journal-title":"NIA-NASA Langley National Institute of Aerospace Hampton VA Report NIA Report"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"article-title":"Ko-diak: An implementation framework for branch and bound algorithms","year":"2015","author":"smith","key":"ref25"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","start":{"date-parts":[[2019,10,22]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894252.pdf?arnumber=8894252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T18:45:15Z","timestamp":1598208315000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894252\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":34,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894252","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}