{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:15Z","timestamp":1772163975603,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,4,18]]},"DOI":"10.1145\/1217935.1217943","type":"proceedings-article","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T15:41:00Z","timestamp":1175787660000},"page":"73-85","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":183,"title":["Thorough static analysis of device drivers"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Ella","family":"Bounimova","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Vladimir","family":"Levin","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Jakob","family":"Lichtenberg","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Con","family":"McGarvey","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Bohus","family":"Ondrusek","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]},{"given":"Abdullah","family":"Ustuner","sequence":"additional","affiliation":[{"name":"Microsoft Corporation"}]}],"member":"320","published-online":{"date-parts":[[2006,4,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_30"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"CAV 04: Computer-Aided Verification","author":"Ball T.","year":"2004","unstructured":"T. Ball , B. Cook , S. K. Lahiri , and L. Zhang . Zapato: Automatic theorem proving for predicate abstraction refinement . In CAV 04: Computer-Aided Verification , pages 457 -- 461 , 2004 . T. Ball, B. Cook, S. K. Lahiri, and L. Zhang. Zapato: Automatic theorem proving for predicate abstraction refinement. In CAV 04: Computer-Aided Verification, pages 457--461, 2004."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604140"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.759192"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694618"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672077"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380932"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379690"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/776816.776863"},{"key":"e_1_3_2_1_14_1","volume-title":"NDSS 04: Network and Distributed System Security Symposium","author":"Chen H.","year":"2004","unstructured":"H. Chen , D. Dean , and D. Wagner . Model checking one million lines of c code . In NDSS 04: Network and Distributed System Security Symposium , 2004 . H. Chen, D. Dean, and D. Wagner. Model checking one million lines of c code. In NDSS 04: Network and Distributed System Security Symposium, 2004."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502042"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"CAV 00: Computer Aided Verification","author":"Clarke E.","year":"2000","unstructured":"E. Clarke , O. Grumberg , S. Jha , Y. Lu , and H. Veith . Counterexample-guided abstraction refinement . In CAV 00: Computer Aided Verification , pages 154 -- 169 , 2000 . E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer Aided Verification, pages 154--169, 2000."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_23"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_30"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_9"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_8"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349309"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_3_2_1_29_1","first-page":"1","volume-title":"OSDI 00: Operating System Design and Implementation","author":"Engler D.","year":"2000","unstructured":"D. Engler , B. Chelf , A. Chou , and S. Hallem . Checking system rules using system-specific, programmer-written compiler extensions . In OSDI 00: Operating System Design and Implementation , pages 1 -- 16 . Usenix Association , 2000 . D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation, pages 1--16. Usenix Association, 2000."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_17"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_32_1","volume-title":"OASIS'04: Workshop on Operating System and Architectural Support for the on demand IT InfraStructure","author":"Fraser K.","year":"2004","unstructured":"K. Fraser , S. Hand , R. Neugebauer , I. Pratt , A. Warfield , and M. Williams . Safe hardware access with the Xen virtual machine monitor . In OASIS'04: Workshop on Operating System and Architectural Support for the on demand IT InfraStructure , June 2004 . K. Fraser, S. Hand, R. Neugebauer, I. Pratt, A. Warfield, and M. Williams. Safe hardware access with the Xen virtual machine monitor. In OASIS'04: Workshop on Operating System and Architectural Support for the on demand IT InfraStructure, June 2004."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512539"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_36_1","volume-title":"Princeton University Press","author":"Kurshan R. P.","year":"1994","unstructured":"R. P. Kurshan . Computer-aided Verification of Coordinating Processes . Princeton University Press , 1994 . R. P. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_5"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2004.1293079"},{"key":"e_1_3_2_1_40_1","first-page":"302","volume-title":"CC 98: Compiler Construction","author":"Leino K. R. M.","year":"1998","unstructured":"K. R. M. Leino and G. Nelson . An extended static checker for Modula-3 . In CC 98: Compiler Construction , pages 302 -- 305 , 1998 . K. R. M. Leino and G. Nelson. An extended static checker for Modula-3. In CC 98: Compiler Construction, pages 302--305, 1998."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503286"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996845"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945466"},{"key":"e_1_3_2_1_45_1","first-page":"332","volume-title":"LICS 86: Logic in Computer Science","author":"Vardi M. Y.","year":"1996","unstructured":"M. Y. Vardi and P. Wolper . An automata theoretic apporach to automatic program verification . In LICS 86: Logic in Computer Science , pages 332 -- 344 . IEEE Computer Society Press , 1996 . M. Y. Vardi and P. Wolper. An automata theoretic apporach to automatic program verification. In LICS 86: Logic in Computer Science, pages 332--344. IEEE Computer Society Press, 1996."}],"event":{"name":"EUROSYS06: Eurosys 2006 Conference","location":"Leuven Belgium","acronym":"EUROSYS06","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the 1st ACM SIGOPS\/EuroSys European Conference on Computer Systems 2006"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1217935.1217943","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T07:31:54Z","timestamp":1693812714000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1217935.1217943"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4,18]]},"references-count":44,"alternative-id":["10.1145\/1217935.1217943","10.1145\/1217935"],"URL":"https:\/\/doi.org\/10.1145\/1217935.1217943","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1218063.1217943","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2006,4,18]]},"assertion":[{"value":"2006-04-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}