@inproceedings(Adya_HTBD_02,
 author       = "A. Adya and J. Howell and M. Theimer and W. Bolosky and J. Douceur",
 year         = "2002",
 title        = "Cooperative task management without manual stack management",
 booktitle    = "2002 USENIX",
 address      = "Monterey, CA, USA",
 pages        = "289--302",
)
@techreport(Amani_CDLRZ_12_,
 author       = "Sidney Amani and Peter Chubb and Alastair Donaldson and Alexander Legg and Leonid Ryzhyk and Yanjin Zhu",
 year         = "2012",
 title        = "Active Device Drivers",
 type         = "NICTA Technical Report",
 institution  = "NICTA",
 note         = "\url {http://www.cse.unsw.edu.au/~leonidr/publications/Amani_CDLRZ_12.pdf}",
)
@inproceedings(Ball_BCLLMORU_06,
 author       = "Thomas Ball and Ella Bounimova and Byron Cook and Vladimir Levin and Jakob Lichtenberg and Con McGarvey and Bohus Ondrusek and Sriram K. Rajamani and Abdullah Ustuner",
 year         = "2006",
 title        = "Thorough Static Analysis of Device Drivers",
 booktitle    = "1st EuroSys Conf.",
 address      = "Leuven, Belgium",
 pages        = "73--85",
 doi          = "10.1145/1217935.1217943",
)
@article(Barnes_Ritson_09,
 author       = "Fred Barnes and Carl Ritson",
 year         = "2009",
 title        = "Checking Process-Oriented Operating System Behaviour Using {CSP} and Refinement",
 journal      = "Operat. Syst. Rev.",
 volume       = "43",
 number       = "4",
 pages        = "45--49",
 doi          = "10.1145/1713254.1713265",
)
@inproceedings(DBLP:conf/tacas/BaslerHKOWZ10,
 author       = "G{\'e}rard Basler and Matthew Hague and Daniel Kroening and C.-H. Luke Ong and Thomas Wahl and Haoxian Zhao",
 year         = "2010",
 title        = "Boom: Taking Boolean Program Model Checking One Step Further",
 booktitle    = "TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "6015",
 publisher    = "Springer",
 pages        = "145--149",
 doi          = "10.1007/978-3-642-12002-2\_11",
)
@inproceedings(Chandrasekaran_CJR_07,
 author       = "Prakash Chandrasekaran and Christopher L. Conway and Joseph M. Joy and Sriram K. Rajamani",
 year         = "2007",
 title        = "Programming asynchronous layers with {CLARITY}",
 booktitle    = "6th ESEC",
 address      = "Dubrovnik, Croatia",
 pages        = "65--74",
)
@inproceedings(Chou_YCHE_01,
 author       = "Andy Chou and Jun-Feng Yang and Benjamin Chelf and Seth Hallem and Dawson Engler",
 year         = "2001",
 title        = "An Empirical Study of Operating Systems Errors",
 booktitle    = "18th SOSP",
 address      = "Lake Louise, Alta, Canada",
 pages        = "73--88",
)
@article(Clarke_KSY_04_,
 author       = "Edmund M. Clarke and Daniel Kroening and Natasha Sharygina and Karen Yorav",
 year         = "2004",
 title        = "Predicate Abstraction of {ANSI-C} Programs Using {SAT}",
 journal      = "Formal Methods in System Design",
 volume       = "25",
 number       = "2-3",
 pages        = "105--127",
 doi          = "10.1023/B:FORM.0000040025.89719.f3",
)
@inproceedings(Cook_PR_06,
 author       = "Byron Cook and Andreas Podelski and Andrey Rybalchenko",
 year         = "2006",
 title        = "Termination proofs for systems code",
 booktitle    = "2006 PLDI",
 address      = "Ottawa, Ontario, Canada",
 pages        = "415--426",
 doi          = "10.1145/1133981.1134029",
)
@book(ClGrPe,
 author       = "Doron Peled Edmund M. Clarke, Orna Grumberg",
 year         = "1999",
 title        = "Model Checking",
 publisher    = "MIT Press",
)
@inproceedings(Engler_CCH_00_,
 author       = "Dawson R. Engler and Benjamin Chelf and Andy Chou and Seth Hallem",
 year         = "2000",
 title        = "Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions",
 booktitle    = "4th OSDI",
 pages        = "1--16",
)
@inproceedings(Fahndrich_AHHHRL_06,
 author       = "Manuel F\"ahndrich and Mark Aiken and Chris Hawblitzel and Orion Hodson and Galen C. Hunt and James R. Larus and Steven Levi",
 year         = "2006",
 title        = "Language Support for Fast and Reliable Message-Based Communication in {Singularity} {OS}",
 booktitle    = "1st EuroSys Conf.",
 address      = "Leuven, Belgium",
 pages        = "177--190",
 doi          = "10.1145/1217935.1217953",
)
@inproceedings(Fehnker_HJLR_06,
 author       = "Ansgar Fehnker and Ralf Huuck and Patrick Jayet and Michel Lussenburg and Felix Rauch",
 year         = "2006",
 title        = "Goanna --- {A Static Model Checker}",
 booktitle    = "11th FMICS",
 address      = "Bonn, Germany",
 pages        = "297--300",
)
@inproceedings(Ganapathi_GP_06,
 author       = "Archana Ganapathi and Viji Ganapathi and David Patterson",
 year         = "2006",
 title        = "{Windows XP} Kernel Crash Analysis",
 booktitle    = "20th LISA",
 address      = "Washington, DC, USA",
 pages        = "101--111",
)
@article(Harel_87,
 author       = "David Harel",
 year         = "1987",
 title        = "{Statecharts}: A Visual Formalism for Complex Systems",
 journal      = "Science of Computer Programming",
 volume       = "8",
 number       = "3",
 pages        = "231--274",
 doi          = "10.1016/0167-6423(87)90035-9",
)
@inproceedings(Henzinger_JMNSW_02,
 author       = "Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and George C. Necula and Gr\'{e}goire Sutre and Westley Weimer",
 year         = "2002",
 title        = "Temporal-Safety Proofs for Systems Code",
 booktitle    = "14th CAV",
 address      = "Copenhagen, Denmark",
 pages        = "526--538",
)
@inproceedings(Holzmann_00,
 author       = "Gerard J. Holzmann",
 year         = "2000",
 title        = "Logic Verification of {ANSI-C} Code with {SPIN}",
 booktitle    = "7th SPIN",
 pages        = "131--147",
)
@book(Holzmann:spin,
 author       = "Gerard J. Holzmann",
 year         = "2003",
 title        = "The {SPIN} Model Checker: Primer and Reference Manual",
 edition      = "1st",
 publisher    = "Addison-Wesley Professional",
)
@article(Hughes_CD_05,
 author       = "Richard Hughes-Jones and Peter Clarke and Steven Dallison",
 year         = "2005",
 title        = "Performance of 1 and 10 {Gigabit} {Ethernet} cards with server quality motherboards",
 journal      = "Future Generation Computer Systems",
 volume       = "21",
 number       = "4",
 pages        = "469--488",
 doi          = "10.1016/j.future.2004.10.002",
)
@book(M93,
 author       = "Kenneth McMillan",
 year         = "1993",
 title        = "Symbolic Model Checking: An Approach to the State Explosion Problem",
 publisher    = "Kluwer Academic",
)
@inproceedings(Ryzhyk_CKH_09,
 author       = "Leonid Ryzhyk and Peter Chubb and Ihor Kuz and Gernot Heiser",
 year         = "2009",
 title        = "Dingo: Taming Device Drivers",
 booktitle    = "4th EuroSys Conf.",
 address      = "Nuremberg, Germany",
)
@inproceedings(Witkowski_BKW_07,
 author       = "Thomas Witkowski and Nicolas Blanc and Daniel Kroening and Georg Weissenbacher",
 year         = "2007",
 title        = "Model checking concurrent {Linux} device drivers",
 booktitle    = "22nd ASE",
 address      = "Atlanta, Georgia, USA",
 pages        = "501--504",
)