{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:06:37Z","timestamp":1761581197964,"version":"3.41.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,5,15]],"date-time":"2014-05-15T00:00:00Z","timestamp":1400112000000},"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":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2014,5,15]]},"abstract":"<jats:p>We develop a practical solution to the problem of automatic verification of the interface between device drivers and the operating system. Our solution relies on a combination of improved driver architecture and verification tools. Unlike previous proposals for verification-friendly drivers, our methodology supports drivers written in C and can be implemented in any existing OS. Our Linuxbased evaluation shows that this methodology amplifies the power of existing model checking tools in detecting driver bugs, making it possible to verify properties that are beyond the reach of traditional techniques.<\/jats:p>","DOI":"10.1145\/2626401.2626424","type":"journal-article","created":{"date-parts":[[2014,5,20]],"date-time":"2014-05-20T13:47:43Z","timestamp":1400593663000},"page":"106-118","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Automatic verification of active device drivers"],"prefix":"10.1145","volume":"48","author":[{"given":"Sidney","family":"Amani","sequence":"first","affiliation":[{"name":"NICTA and University of New South Wales"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Chubb","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Legg","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keng Chai","family":"Ong","sequence":"additional","affiliation":[{"name":"NICTA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanjin","family":"Zhu","sequence":"additional","affiliation":[{"name":"NICTA and University of New South Wales"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,5,15]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"289","volume-title":"USA","author":"ADYA A.","year":"2002"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/1217935.1217943"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-540-24730-2_30"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1145\/1713254.1713265"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/978-3-642-28756-5_47"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1007\/978-3-642-12002-2_11"},{"volume-title":"The esterel synchronous programming language: Design, semantics, implementation","year":"1992","author":"BERRY G.","key":"e_1_2_1_7_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1145\/1287624.1287636"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/502034.502042"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/1133981.1134029"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/2491956.2462184"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_2_1_14_1","first-page":"297","volume-title":"11th FMICS (Bonn","author":"FEHNKER A.","year":"2006"},{"key":"e_1_2_1_15_1","first-page":"101","volume-title":"USA","author":"GANAPATHI A.","year":"2006"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1016\/0167-6423(87)90035-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.5555\/647771.734280"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.5555\/645880.672083"},{"key":"e_1_2_1_19_1","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"HOLZMANN G. J.","year":"2003","edition":"1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/122120.122124"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/1352592.1352618"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/1950365.1950401"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1145\/1519065.1519095"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1145\/1519065.1519095"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1145\/1321631.1321719"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2626401.2626424","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2626401.2626424","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:42Z","timestamp":1750231182000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2626401.2626424"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,15]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,5,15]]}},"alternative-id":["10.1145\/2626401.2626424"],"URL":"https:\/\/doi.org\/10.1145\/2626401.2626424","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2014,5,15]]},"assertion":[{"value":"2014-05-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}