\begin{thebibliography}{10}

\bibitem{clocutility}
{Al Danial}.
\newblock {CLOC}: {Count} lines of code.
\newblock \url{http://cloc.sourceforge.net/}, 2010.

\bibitem{amani:static-driver:apsys:2011}
S.~Amani, L.~Ryzhyk, A.~Donaldson, G.~Heiser, A.~Legg, and Y.~Zhu.
\newblock Static analysis of device drivers: {We} can do better!
\newblock In {\em Proceedings of the 2nd ACM SIGOPS Asia-Pacific Workshop on
  Systems}, 2011.

\bibitem{bbc+06}
T.~Ball, E.~Bounimova, B.~Cook, V.~Levin, J.~Lichtenberg, et~al.
\newblock Thorough static analysis of device drivers.
\newblock In {\em EuroSys '06}, 2006.

\bibitem{Ball:2011:DSM:1965724.1965743}
T.~Ball, V.~Levin, and S.~K. Rajamani.
\newblock \href{http://doi.acm.org/10.1145/1965724.1965743}{A decade of
  software model checking with {SLAM}}.
\newblock In {\em Commun. of the ACM}, volume~54, July 2011.

\bibitem{br02}
T.~Ball and S.~K. Rajamani.
\newblock The {SLAM} project: {Debugging} system software via static analysis.
\newblock In {\em POPL 2002}.

\bibitem{Barnett:2011:SVS:1953122.1953145}
M.~Barnett, M.~F\"{a}hndrich, K.~R.~M. Leino, P.~M\"{u}ller, W.~Schulte, and
  H.~Venter.
\newblock \href{http://doi.acm.org/10.1145/1953122.1953145}{Specification and
  verification: {T}he {Spec\#} experience}.
\newblock In {\em Commun. of the ACM}, volume~54, June 2011.

\bibitem{b05b}
F.~Bellard.
\newblock {QEMU}, a fast and portable dynamic translator.
\newblock In {\em USENIX ATC 2005}.

\bibitem{Bessey:2010:FBL:1646353.1646374}
A.~Bessey, K.~Block, B.~Chelf, A.~Chou, B.~Fulton, S.~Hallem, C.~Henri-Gros,
  A.~Kamsky, S.~McPeak, and D.~Engler.
\newblock \href{http://doi.acm.org/10.1145/1646353.1646374}{A few billion lines
  of code later: {Using} static analysis to find bugs in the real world}.
\newblock {\em Commun. ACM}, 53:66--75, February 2010.

\bibitem{bel75}
R.~S. Boyer, B.~Elspas, and K.~N. Levitt.
\newblock {SELECT}---{A} formal system for testing and debugging programs by
  symbolic execution.
\newblock In {\em Intl. Conf. on Reliable Software, 1975}.

\bibitem{cde08}
C.~Cadar, D.~Dunbar, and D.~Engler.
\newblock
  \href{http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar_html/}{{KLEE}: Unassisted and automatic generation of high-coverage tests for
  complex systems programs}.
\newblock In {\em OSDI 2008}.

\bibitem{cgp08}
C.~Cadar, V.~Ganesh, P.~Pawlowski, D.~Dill, and D.~Engler.
\newblock {EXE}: {Automatically} generating inputs of death.
\newblock {\em In ACM Transactions on Information and System Security}, 2008.

\bibitem{chen:linux-vuln:apsys:2011}
H.~Chen, Y.~Mao, X.~Wang, D.~Zhou, N.~Zeldovich, and M.~F. Kaashoek.
\newblock {Linux} kernel vulnerabilities: {State-of-the-art} defenses and open
  problems.
\newblock In {\em Proceedings of the 2nd ACM SIGOPS Asia-Pacific Workshop on
  Systems}, 2011.

\bibitem{chipounov2009selective}
V.~Chipounov, V.~Georgescu, C.~Zamfir, and G.~Candea.
\newblock {Selective symbolic execution}.
\newblock In {\em HotDep}, 2009.

\bibitem{ckc11}
V.~Chipounov, V.~Kuznetsov, and G.~Candea.
\newblock \href{http://doi.acm.org/10.1145/1950365.1950396}{{S2E}: {A} platform
  for in-vivo multi-path analysis of software systems}.
\newblock In {\em ASPLOS 2011}.

\bibitem{ckc12}
V.~Chipounov, V.~Kuznetsov, and G.~Candea.
\newblock \href{http://doi.acm.org/10.1145/2110356.2110358}{The {S2E} platform:
  {D}esign, implementation, and applications}.
\newblock {\em ACM Trans. Comput. Syst.}, 30(1):2:1--2:49, Feb. 2012.

\bibitem{cfb06}
M.~Cova, V.~Felmetsger, G.~Banks, and G.~Vigna.
\newblock Static detection of vulnerabilities in x86 executables.
\newblock In {\em ACSAC 2006}.

\bibitem{coverity04}
Coverity.
\newblock Analysis of the {Linux} kernel, 2004.
\newblock Available at \url{http://www.coverity.com}.

\bibitem{cbz11}
O.~Crameri, R.~Bianchini, and W.~Zwaenepoel.
\newblock \href{http://doi.acm.org/10.1145/1966445.1966464}{Striking a new
  balance between program instrumentation and debugging time}.
\newblock In {\em EuroSys 2011}.

\bibitem{ecch00}
D.~R. Engler, B.~Chelf, A.~Chou, and S.~Hallem.
\newblock Checking system rules using system-specific, programmer-written
  compiler extensions.
\newblock In {\em OSDI 2000}.

\bibitem{gks05}
P.~Godefroid, N.~Klarlund, and K.~Sen.
\newblock {DART}: {D}irected automated random testing.
\newblock In {\em PLDI '05}, 2005.

\bibitem{glm08}
P.~Godefroid, M.~Levin, D.~Molnar, et~al.
\newblock {Automated whitebox fuzz testing}.
\newblock In {\em NDSS 2008}.

\bibitem{stableapinonsense}
{Greg Kroah-Hartman}.
\newblock The {Linux} kernel driver interface.
\newblock
  \url{http://www.kernel.org/doc/Documentation/stable_api_nonsense.txt}, 2011.

\bibitem{graal08}
H.~Gunawi, C.~Rubio-Gonz{\'a}lez, A.~Arpaci-Dusseau, R.~Arpaci-Dusseau, and
  B.~Liblit.
\newblock {EIO: Error handling is occasionally correct}.
\newblock In {\em 6th USENIX FAST}, 2008.

\bibitem{ltp10}
{IBM}.
\newblock {Linux} test project.
\newblock \url{http://ltp.sourceforge.net/}, May 2010.

\bibitem{krs09}
A.~Kadav, M.~J. Renzelmann, and M.~M. Swift.
\newblock Tolerating hardware device failures in software.
\newblock In {\em SOSP}, 2009.

\bibitem{kcc10}
V.~Kuznetsov, V.~Chipounov, and G.~Candea.
\newblock Testing closed-source binary device drivers with {DDT}.
\newblock In {\em USENIX ATC}, 2010.

\bibitem{la03}
E.~Larson and T.~Austin.
\newblock {High coverage detection of input-related security facults}.
\newblock In {\em USENIX Security}, 2003.

\bibitem{ms07}
R.~Majumdar and K.~Sen.
\newblock Hybrid concolic testing.
\newblock In {\em ICSE 2007}.

\bibitem{windows-device-testing}
{Microsoft}.
\newblock Windows device testing framework design guide.
\newblock
  \url{http://msdn.microsoft.com/en-us/library/windows/hardware/ff539645\%28v=vs.85\%29.aspx}, 2011.

\bibitem{microsoft05b}
{Microsoft Corporation}.
\newblock How to use driver verifier to troubleshoot windows drivers.
\newblock \url{http://support.microsoft.com/kb/q244617/}, Jan. 2005.
\newblock Knowledge Base Article Q244617.

\bibitem{microsoft10}
{Microsoft Corporation}.
\newblock {S}tatic {D}river {V}erifier.
\newblock \url{http://www.microsoft.com/whdc/devtools/ tools/sdv.mspx}, May
  2010.

\bibitem{nmr+02}
G.~C. Necula, S.~Mcpeak, S.~P. Rahul, and W.~Weimer.
\newblock {CIL:} {Intermediate} language and tools for analysis and
  transformation of {C} programs.
\newblock In {\em Intl. Conf. on Compiler Constr.}, 2002.

\bibitem{nelson:driver-model:plumbers:2011}
S.~Nelson and P.~Waskiewicz.
\newblock Virtualization: Writing (and testing) device drivers without
  hardware.
\newblock \url{www.linuxplumbersconf.org/2011/ocw/sessions/243}, 2011.
\newblock Linux Plumbers Conference.

\bibitem{ns07}
N.~Nethercode and J.~Seward.
\newblock {Valgrind}: {A} framework for heavyweight dynamic binary
  instrumentation.
\newblock In {\em PLDI}, 2007.

\bibitem{padioleau:coccinelle:eurosys:2008}
Y.~Padioleau, J.~Lawall, R.~R. Hansen, and G.~Muller.
\newblock Documenting and automating collateral evolutions in {Linux} device
  drivers.
\newblock In {\em EuroSys 2008}.

\bibitem{pyr11}
S.~Person, G.~Yang, N.~Rungta, and S.~Khurshid.
\newblock Directed incremental symbolic execution.
\newblock In {\em PLDI 2011}.

\bibitem{Pasareanu:2008:CUS:1390630.1390635}
C.~S. P\v{a}s\v{a}reanu~et al.
\newblock Combining unit-level symbolic execution and system-level concrete
  execution for testing {NASA} software.
\newblock In {\em ISSTA 2008}.

\bibitem{ryzhyk:formalize-dd:plos:2007}
L.~Ryzhyk, I.~Kuz, and G.~Heiser.
\newblock Formalising device driver interfaces.
\newblock In {\em Workshop on Programming Languages and Systems}, Oct. 2007.

\bibitem{sma05}
K.~Sen, D.~Marinov, and G.~Agha.
\newblock {CUTE}: {A} concolic unit testing engine for {C}.
\newblock In {\em ESEC/FSE-13}, 2005.

\bibitem{Song:2008:BNA:1496255.1496257}
D.~Song~et al.
\newblock {BitBlaze}: {A} new approach to computer security via binary
  analysis.
\newblock In {\em ICISS 2008}.

\bibitem{susskraut:error-handling:edcc:2006}
M.~Susskraut and C.~Fetzer.
\newblock Automatically finding and patching bad error handling.
\newblock In {\em DSN 2006}.

\bibitem{williams:nexus-drivers:osdi:2008}
D.~Williams, P.~Reynolds, K.~Walsh, E.~G. Sirer, and F.~B. Schneider.
\newblock Device driver safety through a reference validation mechanism.
\newblock In {\em OSDI 2008}.

\bibitem{xmsn05}
T.~Xie, D.~Marinov, W.~Schulte, and D.~Notkin.
\newblock Symstra: A framework for generating object-oriented unit tests using
  symbolic execution.
\newblock In {\em TACAS}, 2005.

\bibitem{yst06}
J.~Yang, C.~Sar, P.~Twohey, C.~Cadar, and D.~Engler.
\newblock \href{http://dx.doi.org/10.1109/SP.2006.7}{Automatically generating
  malicious disks using symbolic execution}.
\newblock In {\em IEEE Symp. on Security and Privacy}, SP '06, 2006. IEEE
  Computer Society.

\bibitem{zamfir10}
C.~Zamfir and G.~Candea.
\newblock Execution synthesis: {A} technique for automated software debugging.
\newblock In {\em EuroSys 2010}.

\end{thebibliography}
