{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:17:11Z","timestamp":1760044631711,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T00:00:00Z","timestamp":1570579200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2297"],"award-info":[{"award-number":["N00014-17-1-2297"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010465","name":"Naval Sea Systems Command","doi-asserted-by":"publisher","award":["N00174-16-C-0018"],"award-info":[{"award-number":["N00174-16-C-0018"]}],"id":[{"id":"10.13039\/100010465","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,10,9]]},"DOI":"10.1145\/3359986.3361215","type":"proceedings-article","created":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T12:21:06Z","timestamp":1570450866000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Establishing a refinement relation between binaries and abstract code"],"prefix":"10.1145","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[{"name":"Virginia Tech"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Bockenek","sequence":"additional","affiliation":[{"name":"Virginia Tech"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abhijith","family":"Bharadwaj","sequence":"additional","affiliation":[{"name":"Virginia Tech"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[{"name":"Virginia Tech"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Roessle","sequence":"additional","affiliation":[{"name":"Joint Artificial Intelligence Center"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,9]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"362","volume-title":"Software verification with ITPs should use binary code extraction to reduce the TCB,\" in International Conference on Interactive Theorem Proving","author":"Kumar R.","year":"2018","unstructured":"R. Kumar, E. Mullen, Z. Tatlock, and M. O. Myreen, \"Software verification with ITPs should use binary code extraction to reduce the TCB,\" in International Conference on Interactive Theorem Proving. Springer, 2018, pp. 362--369."},{"key":"e_1_3_2_1_2_1","first-page":"1","article-title":"Machine-code verification for multiple architectures - an application of decompilation into logic,\" in 2008 Formal Methods","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 2008 Formal Methods in Computer-Aided Design, Nov 2008, pp. 1--8.","journal-title":"Computer-Aided Design"},{"key":"e_1_3_2_1_3_1","first-page":"78","article-title":"Decompilation into logic - Improved,\" in Formal Methods in Computer-Aided Design (FMCAD), 2012","author":"Myreen M. O.","year":"2012","unstructured":"M. O. Myreen, M. J. Gordon, and K. Slind, \"Decompilation into logic - Improved,\" in Formal Methods in Computer-Aided Design (FMCAD), 2012. IEEE, 2012, pp. 78--81.","journal-title":"IEEE"},{"key":"e_1_3_2_1_4_1","volume-title":"INRIA Paris-Rocquencourt","author":"Leroy X.","year":"2012","unstructured":"X. Leroy et al., \"The CompCert verified compiler,\" Documentation and user\u00e2\u0102Źs manual. INRIA Paris-Rocquencourt, 2012."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/907044"},{"key":"e_1_3_2_1_7_1","first-page":"151","volume-title":"Translation validation,\" in International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Pnueli A.","year":"1998","unstructured":"A. Pnueli, M. Siegel, and E. Singerman, \"Translation validation,\" in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 1998, pp. 151--166."},{"key":"e_1_3_2_1_8_1","first-page":"471","volume-title":"ACM","author":"Sewell T. A. L.","year":"2013","unstructured":"T. A. L. Sewell, M. O. Myreen, and G. Klein, \"Translation validation for a verified os kernel,\" in ACM SIGPLAN Notices, vol. 48, no. 6. ACM, 2013, pp. 471--482."},{"key":"e_1_3_2_1_9_1","volume-title":"Ramblr: Making reassembly great again,\" in Proceedings of the 24th Annual Symposium on Network and Distributed System Security (NDSS'17)","author":"Wang R.","year":"2017","unstructured":"R. Wang, Y. Shoshitaishvili, A. Bianchi, A. Machiry, J. Grosen, P. Grosen, C. Kruegel, and G. Vigna, \"Ramblr: Making reassembly great again,\" in Proceedings of the 24th Annual Symposium on Network and Distributed System Security (NDSS'17), 2017."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.005"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9360-2"},{"key":"e_1_3_2_1_13_1","first-page":"116","volume-title":"Extending sledgehammer with smt solvers,\" in International Conference on Automated Deduction","author":"Blanchette J. C.","year":"2011","unstructured":"J. C. Blanchette, S. B\u00f6hme, and L. C. Paulson, \"Extending sledgehammer with smt solvers,\" in International Conference on Automated Deduction. Springer, 2011, pp. 116--130."},{"key":"e_1_3_2_1_14_1","first-page":"337","volume-title":"Z3: An efficient smt solver,\" in International conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"De Moura L.","year":"2008","unstructured":"L. De Moura and N. Bj\u00f8rner, \"Z3: An efficient smt solver,\" in International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337--340."},{"key":"e_1_3_2_1_15_1","first-page":"171","volume-title":"Cvc4,\" in International Conference on Computer Aided Verification","author":"Barrett C.","year":"2011","unstructured":"C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi\u0107, T. King, A. Reynolds, and C. Tinelli, \"Cvc4,\" in International Conference on Computer Aided Verification. Springer, 2011, pp. 171--177."},{"key":"e_1_3_2_1_16_1","first-page":"83","volume-title":"ACM","author":"Necula G. C.","year":"2000","unstructured":"G. C. Necula, \"Translation validation for an optimizing compiler,\" in ACM sigplan notices, vol. 35, no. 5. ACM, 2000, pp. 83--94."},{"key":"e_1_3_2_1_17_1","first-page":"54","volume-title":"ACM","author":"Chlipala A.","year":"2007","unstructured":"A. Chlipala, \"A certified type-preserving compiler from lambda calculus to assembly language,\" in ACM Sigplan Notices, vol. 42, no. 6. ACM, 2007, pp. 54--65."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_19_1","first-page":"107","volume-title":"ACM","author":"Myreen M. O.","year":"2010","unstructured":"M. O. Myreen, \"Verified just-in-time compiler on x86,\" in ACM Sigplan Notices, vol. 45, no. 1. ACM, 2010, pp. 107--118."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9317-x"},{"volume-title":"SSS'17","author":"K\u00e4stner D.","key":"e_1_3_2_1_21_1","unstructured":"D. K\u00e4stner, X. Leroy, S. Blazy, B. Schommer, M. Schmidt, and C. Ferdinand, \"Closing the gap - the formally verified optimizing compiler CompCert,\" in Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium, ser. SSS'17. Bristol, United Kingdom: Safety-Critical Systems Club, Feb. 2017, pp. 163--180. [Online]. Available: https:\/\/hal.inria.fr\/hal-01399482"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_1_23_1","first-page":"543","volume-title":"Formal C semantics: CompCert and the C standard,\" in International Conference on Interactive Theorem Proving","author":"Krebbers R.","year":"2014","unstructured":"R. Krebbers, X. Leroy, and F. Wiedijk, \"Formal C semantics: CompCert and the C standard,\" in International Conference on Interactive Theorem Proving. Springer, 2014, pp. 543--548."},{"key":"e_1_3_2_1_24_1","first-page":"568","volume-title":"Hoare logic for realistically modelled machine code,\" in International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Myreen M. O.","year":"2007","unstructured":"M. O. Myreen and M. J. Gordon, \"Hoare logic for realistically modelled machine code,\" in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2007, pp. 568--582."},{"key":"e_1_3_2_1_25_1","first-page":"272","volume-title":"Hoare logic for arm machine code,\" in International Conference on Fundamentals of Software Engineering","author":"Myreen M. O.","year":"2007","unstructured":"M. O. Myreen, A. C. Fox, and M. J. Gordon, \"Hoare logic for arm machine code,\" in International Conference on Fundamentals of Software Engineering. Springer, 2007, pp. 272--286."},{"key":"e_1_3_2_1_26_1","first-page":"91","volume-title":"FMCAD '14","author":"Goel S.","year":"2014","unstructured":"S. Goel, W. A. Hunt, M. Kaufmann, and S. Ghosh, \"Simulation and formal verification of x86 machine-code programs that make system calls,\" in Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, ser. FMCAD '14. Austin, TX: FMCAD Inc, 2014, pp. 18:91--18:98. [Online]. Available: http:\/\/dl.acm.org\/citation.cfm?id=2682923.2682944"},{"key":"e_1_3_2_1_27_1","first-page":"362","volume-title":"Artificial Intelligence","author":"Matthews J.","year":"2006","unstructured":"J. Matthews, J. S. Moore, S. Ray, and D. Vroon, \"Verification condition generation via theorem proving,\" in International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, 2006, pp. 362--376."}],"event":{"name":"MEMOCODE '19: 17th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"La Jolla California","acronym":"MEMOCODE '19"},"container-title":["Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359986.3361215","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3359986.3361215","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3359986.3361215","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:27Z","timestamp":1750202007000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359986.3361215"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,9]]},"references-count":27,"alternative-id":["10.1145\/3359986.3361215","10.1145\/3359986"],"URL":"https:\/\/doi.org\/10.1145\/3359986.3361215","relation":{},"subject":[],"published":{"date-parts":[[2019,10,9]]},"assertion":[{"value":"2019-10-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}