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