{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:26:48Z","timestamp":1750220808636,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,11,15]],"date-time":"2019-11-15T00:00:00Z","timestamp":1573776000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1513704"],"award-info":[{"award-number":["1513704"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-15-C-0066"],"award-info":[{"award-number":["FA8750-15-C-0066"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N0014-17-1-2995"],"award-info":[{"award-number":["N0014-17-1-2995"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-19-C-0006"],"award-info":[{"award-number":["FA8750-19-C-0006"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,11,15]]},"DOI":"10.1145\/3338502.3359759","type":"proceedings-article","created":{"date-parts":[[2019,11,8]],"date-time":"2019-11-08T13:40:33Z","timestamp":1573220433000},"page":"25-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Source-free Machine-checked Validation of Native Code in Coq"],"prefix":"10.1145","author":[{"given":"Kevin W.","family":"Hamlen","sequence":"first","affiliation":[{"name":"University of Texas at Dallas, Richardson, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dakota","family":"Fisher","sequence":"additional","affiliation":[{"name":"University of Texas at Dallas, Richardson, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilmore R.","family":"Lundquist","sequence":"additional","affiliation":[{"name":"University of Texas at Dallas, Richardson, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,11,15]]},"reference":[{"volume-title":"Proceedings of the cnum23rd International Conference on Computer Aided Verification nymCAV. 463--469","author":"Brumley David","key":"e_1_3_2_1_1_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.6.801"},{"volume-title":"Proceedings of the cnum26th ACM Conference on Computer and Communications Security nymCCS. forthcoming.","author":"Ghaffarinia Masoud","key":"e_1_3_2_1_5_1"},{"volume-title":"Proceedings of the cnum11th USENIX Security Symposium. 191--206","author":"Kiriansky Vladimir","key":"e_1_3_2_1_6_1"},{"volume-title":"Proceedings of the cnum8th European Congress on Embedded Real Time software and Systems nymERTS$^2$.","year":"2016","author":"Leroy Xavier","key":"e_1_3_2_1_7_1"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792248"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"volume-title":"Proceedings of the cnum28th USENIX Security Symposium. 1733--1750","year":"2019","author":"Qian Chenxiong","key":"e_1_3_2_1_11_1"},{"volume-title":"Proceedings of the cnum11th Asian Computing Science Conference on Advances in Computer Science: Secure Software and Related Issues. 316--330","year":"2006","author":"Tsai Ming-Hsien","key":"e_1_3_2_1_12_1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2420950.2420995"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.25"},{"volume-title":"Proceedings of the cnum22nd USENIX Security Symposium. 337--352","author":"Zhang Mingwei","key":"e_1_3_2_1_16_1"}],"event":{"name":"CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"London United Kingdom","acronym":"CCS '19"},"container-title":["Proceedings of the 3rd ACM Workshop on Forming an Ecosystem Around Software Transformation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3338502.3359759","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3338502.3359759","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3338502.3359759","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:49Z","timestamp":1750201969000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3338502.3359759"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,15]]},"references-count":16,"alternative-id":["10.1145\/3338502.3359759","10.1145\/3338502"],"URL":"https:\/\/doi.org\/10.1145\/3338502.3359759","relation":{},"subject":[],"published":{"date-parts":[[2019,11,15]]},"assertion":[{"value":"2019-11-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}