{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,26]],"date-time":"2026-06-26T09:40:57Z","timestamp":1782466857451,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,10,11]],"date-time":"2009-10-11T00:00:00Z","timestamp":1255219200000},"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":[[2009,10,11]]},"DOI":"10.1145\/1629575.1629583","type":"proceedings-article","created":{"date-parts":[[2009,10,13]],"date-time":"2009-10-13T15:11:11Z","timestamp":1255446671000},"page":"73-86","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":75,"title":["Automatic device driver synthesis with termite"],"prefix":"10.1145","author":[{"given":"Leonid","family":"Ryzhyk","sequence":"first","affiliation":[{"name":"NICTA, UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Chubb","sequence":"additional","affiliation":[{"name":"NICTA, UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ihor","family":"Kuz","sequence":"additional","affiliation":[{"name":"NICTA, UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Etienne","family":"Le Sueur","sequence":"additional","affiliation":[{"name":"NICTA, UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"NICTA, UNSW, Open Kernel Labs, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,10,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217943"},{"key":"e_1_3_2_1_2_1","volume-title":"4th HotDep","author":"Chipounov V.","year":"2008","unstructured":"V. Chipounov and G. Candea . Reverse-engineering drivers for safety and portability . In 4th HotDep , San Diego, CA, USA , Dec 2008 . V. Chipounov and G. Candea. Reverse-engineering drivers for safety and portability. In 4th HotDep, San Diego, CA, USA, Dec 2008."},{"key":"e_1_3_2_1_3_1","volume-title":"Linux kernel security report","author":"Chou A.","year":"2005","unstructured":"A. Chou , B. Fulton , and S. Hallem . Linux kernel security report , 2005 . A. Chou, B. Fulton, and S. Hallem. Linux kernel security report, 2005."},{"key":"e_1_3_2_1_4_1","volume-title":"Microkernel modularity with integrated kernel performance. Technical report","author":"Condict M.","year":"1994","unstructured":"M. Condict , D. Bolinger , D. Mitchell , and E. McManus . Microkernel modularity with integrated kernel performance. Technical report , OSF Research Institute , Jun 1994 . M. Condict, D. Bolinger, D. Mitchell, and E. McManus. Microkernel modularity with integrated kernel performance. Technical report, OSF Research Institute, Jun 1994."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/997163.997169"},{"key":"e_1_3_2_1_6_1","volume-title":"Linux Device Drivers. O'Reilly&Associates","author":"Corbet J.","year":"2005","unstructured":"J. Corbet , A. Rubini , and G. Kroah-Hartman . Linux Device Drivers. O'Reilly&Associates , Inc , 3 rd edition, 2005 . J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux Device Drivers. O'Reilly&Associates, Inc, 3rd edition, 2005.","edition":"3"},{"key":"e_1_3_2_1_7_1","unstructured":"A. Edvardsson. SD card mass storage controller. http:\/\/www.opencores.org.  A. Edvardsson. SD card mass storage controller. http:\/\/www.opencores.org."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251229.1251230"},{"key":"e_1_3_2_1_9_1","first-page":"75","volume-title":"7th OSDI","author":"Erlingsson U.","year":"2006","unstructured":"U. Erlingsson , M. Abadi , M. Vrable , M. Budiu , and G.C. Necula . XFI: software guards for system address spaces . In 7th OSDI , pages 75 -- 88 , Seattle, Washington , Nov 2006 . U. Erlingsson, M. Abadi, M. Vrable, M. Budiu, and G.C. Necula. XFI: software guards for system address spaces. In 7th OSDI, pages 75--88, Seattle, Washington, Nov 2006."},{"key":"e_1_3_2_1_10_1","first-page":"101","volume-title":"20th LISA","author":"Ganapathi A.","year":"2006","unstructured":"A. Ganapathi , V. Ganapathi , and D. Patterson . Windows XP kernel crash analysis . In 20th LISA , pages 101 -- 111 , Washington, DC, USA , 2006 . A. Ganapathi, V. Ganapathi, and D. Patterson. Windows XP kernel crash analysis. In 20th LISA, pages 101--111, Washington, DC, USA, 2006."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759210.1759296"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1151374.1151391"},{"key":"e_1_3_2_1_13_1","unstructured":"IEEE 802.3 Ethernet working group. http:\/\/grouper.ieee.org\/groups\/802\/3\/.  IEEE 802.3 Ethernet working group. http:\/\/grouper.ieee.org\/groups\/802\/3\/."},{"key":"e_1_3_2_1_14_1","unstructured":"LOTOS -- a formal description technique based on the temporal ordering of observational behavior 1989. ISO Standard 8807.  LOTOS -- a formal description technique based on the temporal ordering of observational behavior 1989. ISO Standard 8807."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-005-0654-4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/122120.122124"},{"key":"e_1_3_2_1_17_1","first-page":"17","volume-title":"4th OSDI","author":"M\u00e9rillon F.","year":"2000","unstructured":"F. M\u00e9rillon , L. R\u00e9veill\u00e8re , C. Consel , R. Marlet , and G. Muller . Devil: An IDL for hardware programming . In 4th OSDI , pages 17 -- 30 , San Diego, CA, USA , Oct 2000 . F. M\u00e9rillon, L. R\u00e9veill\u00e8re, C. Consel, R. Marlet, and G. Muller. Devil: An IDL for hardware programming. In 4th OSDI, pages 17--30, San Diego, CA, USA, Oct 2000."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/945405.938257"},{"key":"e_1_3_2_1_19_1","volume-title":"Single-chip multifunction 10\/100mbps Ethernet controller with power management. datasheet","author":"Realtek Corp.","year":"2005","unstructured":"Realtek Corp. Single-chip multifunction 10\/100mbps Ethernet controller with power management. datasheet ., 2005 . Realtek Corp. Single-chip multifunction 10\/100mbps Ethernet controller with power management. datasheet., 2005."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1519065.1519095"},{"key":"e_1_3_2_1_21_1","volume-title":"SD specifications part 1: Physical layer simplified specification, version 2.00","author":"SD Card Association","year":"2006","unstructured":"SD Card Association . SD specifications part 1: Physical layer simplified specification, version 2.00 , 2006 . SD Card Association. SD specifications part 1: Physical layer simplified specification, version 2.00, 2006."},{"key":"e_1_3_2_1_22_1","volume-title":"SD specifications part a2: SD host controller simplified specification, version 2.00","author":"SD Card Association","year":"2007","unstructured":"SD Card Association . SD specifications part a2: SD host controller simplified specification, version 2.00 , 2007 . SD Card Association. SD specifications part a2: SD host controller simplified specification, version 2.00, 2007."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086230"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945466"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59042-0_57"},{"key":"e_1_3_2_1_27_1","volume-title":"40th DATE","author":"Wang S.","year":"2003","unstructured":"S. Wang , S. Malik , and R.A. Bergamaschi . Modeling and integration of peripheral devices in embedded systems . In 40th DATE , 2003 . S. Wang, S. Malik, and R.A. Bergamaschi. Modeling and integration of peripheral devices in embedded systems. In 40th DATE, 2003."},{"key":"e_1_3_2_1_28_1","first-page":"45","volume-title":"7th OSDI","author":"Zhou F.","year":"2006","unstructured":"F. Zhou , J. Condit , Z. Anderson , I. Bagrak , R. Ennals , M. Harren , G. Necula , and E. Brewer . SafeDrive: Safe and recoverable extensions using language-based techniques . In 7th OSDI , pages 45 -- 60 , Seattle, WA, USA , Nov 2006 . F. Zhou, J. Condit, Z. Anderson, I. Bagrak, R. Ennals, M. Harren, G. Necula, and E. Brewer. SafeDrive: Safe and recoverable extensions using language-based techniques. In 7th OSDI, pages 45--60, Seattle, WA, USA, Nov 2006."}],"event":{"name":"SOSP09: ACM SIGOPS 22nd Symposium on Operating Systems Principles","location":"Big Sky Montana USA","acronym":"SOSP09","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1629575.1629583","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1629575.1629583","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:23:27Z","timestamp":1750249407000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1629575.1629583"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10,11]]},"references-count":27,"alternative-id":["10.1145\/1629575.1629583","10.1145\/1629575"],"URL":"https:\/\/doi.org\/10.1145\/1629575.1629583","relation":{},"subject":[],"published":{"date-parts":[[2009,10,11]]},"assertion":[{"value":"2009-10-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}