Device-driver development and testing is a complex and error-prone
undertaking.  For example, testing error-handling code requires
simulating faulty inputs from the device.  A single driver may support
dozens of devices, and a developer may not have access to any of
them. Consequently, many Linux driver patches include the comment
``compile tested only.''

\Arch\ is a system for testing Linux and FreeBSD drivers without their
devices present. The system uses symbolic execution to remove the need
for hardware, and extends past tools with three new features. First,
\Arch\ uses static-analysis and source-to-source transformation to
greatly reduce the effort of testing a new driver. Second, \Arch\ checkers
are ordinary C code and execute in the kernel, where they have full
access to kernel and driver state. Finally, \Arch\ provides an
execution-tracing tool to identify how a patch changes I/O to the
device and to compare device-driver implementations.  In applying
\Arch\ to 21 Linux drivers and 5 FreeBSD drivers, we found
\howmanybugs\ bugs.

% \howmanydrivers = 21 + 5
