The two primary issues discussed in the reviews relate to how novel SymDrive is, and SymDrive's evaluation.  All reviewers except #2 raised the first issue.  Reviewer #1 and #4 specifically mentioned DDT, while reviewer #3 and #5 discussed the issue in more general terms.  We will first discuss the relationship between SymDrive and DDT, followed by a brief discussion of other related work.  Finally, we will address specific questions.

DDT is similar to SymDrive since it also uses symbolic execution to test device drivers.  DDT uses symbolic data for hardware input, and aims to find bugs in device drivers.  Thus, DDT solves many of the same problems as SymDrive.  Nevertheless, DDT's design is significantly different and we believe these differences influence the functionality provided.  The main benefits of SymDrive are:

1. The ability to write rich specifications that leverage execution state.  DDT operates on closed-source binary device drivers, and consequently has comparatively little knowledge of the operating system's execution context.  Although DDT finds several kinds of bugs, DDT probably could not easily support many of SymDrive's checks, such as correct memory allocation flag usage.  Thus, SymDrive's reliance on source code provides it with additional capability not available to DDT.

2. The record/replay trace facility.  SymDrive provides a straightforward mechanism for testing specific driver components thoroughly by fast-forwarding otherwise uninteresting parts of driver code.  DDT instead attempts to exercise the entire driver regardless of the developer's goals.

3. Increased flexibility.  SymDrive provides several mechanisms for interacting with kernel functions, whereas DDT allows only concrete execution of kernel functions via repeated kernel forking.  SymDrive's flexibility enables more general testing strategies, such as finding locations in the driver that depend on particular kernel function implementations that may fail in future kernel revisions.

Although SymDrive's record/replay functionality and its specification testing along different paths are not novel, we believe that testing drivers with these strategies combined with symbolic execution is new.  Device drivers pose unique challenges compared to existing examples of symbolic execution, such as the broad kernel/driver and driver/device interfaces and the unusual properties of kernel-mode execution, and most other existing work in symbolic execution, DDT excepted, does not examine these issues.

Responses to specific inquiries:
- Reviewer #2 asked, "A device driver that followed the structural requirements [of SymDrive] but moved no actual data would pass all of the tests ... right?"  Yes.  SymDrive does not provide a mechanism to verify correct device-specific operation, so SymDrive would not flag these kinds of errors.

- Reviewer #2 said, "[I]t wasn't clear what kind of coverage you achieved 100% of."  We were referring to 100% line coverage since SymDrive does not currently have a mechanism to report path coverage.

- Reviewer #2 asked, "Are these ['structural'] errors actually the more common failures that programmers encounter in building and deploying device drivers in real distributions?"  We believe that "structural errors" are at least as common as bugs related specifically to the device itself.

Finally, we thank all the reviewers for their insightful comments.