Thank you for your detailed reviews.  We will focus first on what is most novel about SymDrive, and then address other specific questions.

Review B,C: Novelty.
Relative to DDT and S2E, SymDrive supports testing a much broader array of driver types with little additional per-driver effort. SymDrive implements this functionality using:  (A) a novel static analysis and code generation tool, SymGen, (B) a new path-selection heuristic that eliminates the need to write an S2E consistency plugin for the full Linux kernel, (C) a test framework to enable creation of fine-grained checkers, and (D) an execution-differencing tool to verify that a driver's behavior remains consistent after applying a refactoring. 

Review C: Comparison to static analysis.
While static analysis approaches can find many similar bugs, SymDrive provides the ability to generate traces, which can be used to debug problems in the driver/device interface, and better supports testing for chipset-specific problems, where differences in how the driver is initialized cause bugs much later in execution.  Writing checkers in C may be more natural to kernel programmers than coding them for static tools.  SymDrive can also verify higher-level properties such as whether the driver interacts with user-mode software correctly.

Review C: Why only 13 drivers?
Setting up a driver and running tests still takes time, and we have not yet written scripts to automatically test drivers in parallel.

Review A: Bugs in the driver/device interface.
These can only be detected with the differencing mechanism. We are exploring the use of device specifications to complement SymDrive.

Review B: Difficulty of S2E consistency plugins.
They require hand coding a function for every function in the driver/kernel interface. Accessing function parameters, return values, and other stack or heap data is tedious because kernel symbols and structure definitions are not available. Consistency models must also encode the semantics of every interface function, rather than just those of interest.  Furthermore, each driver class requires adding support for additional functions.  SymGen automatically generates code for a single consistency model for the whole kernel that avoids this effort.

Review C,D: False negatives.
False negatives can occur, but we have no concrete data on their prevalence. In our experience with known bugs, false negatives stem from three sources: (1) bugs in S2E, KLEE, or the constraint solver, (2) incomplete specification of kernel behavior in the test framework, and (3) insufficient path coverage.  Regarding (3), SymDrive offers a "high coverage mode," that explores as many paths as possible within particular functions. However, this mode may prove inadequate for finding some inter-procedural bugs.

Review E: Did we only write checkers for known bugs?
We developed 42 checkers, and only 8 of them found bugs. We used the experience gained from scanning several thousand mailing list messages to guide our choices of which to implement. If space permits, we can include a full list of our checkers in the final version.

Review B: Races.
SymDrive can find races from interrupts or context switches, but is not nearly as comprehensive as dedicated race detectors like CTrigger.