\section{Conclusions}
\label{section:conclusions}
\Arch\ uses symbolic execution combined with a \tf\ and static
analysis to test Linux and FreeBSD driver code without access to the
corresponding device.  Our results show that \Arch\ can find bugs in
mature driver code of a variety of types, and allow developers to test
driver patches deeply.  Hopefully, \Arch\ will enable more developers
to patch driver code by lowering the barriers to testing. In the
future, we plan to implement an automated testing service for driver
patches that supplements manual code reviews, and investigate applying
\Arch's techniques to other kernel subsystems.

%\fixme{Julia:  still seems not completely trivial to
%  use.  Prhpas better to target maintainers for whom the work is quickly amortized}
\section*{Acknowledgments}
This work is supported by the National Science Foundation grants
CNS-0745517 and CNS-0915363 and by a gift from Google. We would like
to thank the many reviewers who provided detailed feedback on our
work, and for early feedback from Gilles Muller and Julia Lawall. We
would also like to thank the \see\ developers, who provided us a great
platform to build on. Swift has a significant financial interest in
Microsoft.
