In the first review, the author noted the following capabilities of DDT: - symbolic hardware introduced in RWSet, generalized in DDT. * OK - "it looks like SymDrive's checkers roughly correspond to DDT's OS-level checkers (like the way MSDV was used in DDT); the DDT page says one can plug any checkers into DDT, and they can operate both at the VM level and the OS kernel level." * The DDT paper alludes to an annotation that they rely upon "in our DDT prototype to cooperate with the Microsoft Driver Verifier’s dynamic checkers." * They mention comparing their results against those of Driver Verifier running concretely. * They say, "While testing drivers with DDT can be completely automated, our current DDT prototype requires some manual effort. A developer must provide DDT with PCI device information for the driver’s device, install the driver inside a VM, and configure Microsoft Driver Verifier and a concrete workload generator." * The design section suggests that it's possible to use MSDV-like tools, but does not specifically mention MSDV. * Speculation: They may be running the driver with the dynamic Driver Verifier inside the virtual machine, and then since they fork the entire VM, they also fork Driver Verifier. This would allow them to use DV with DDT. If this is what they're doing it's not at all clear from the text. * Conclusion: It's not clear that they use Driver Verifier for anything meaningful with DDT. - "[Testing driver equivalence is something] the DDT project claims to be able to do, using its execution traces." * The execution trace concept discussed in DDT is apparently a log of a particular execution path through the driver. It's unclear whether this trace includes details of all hardware operations along that path.