User-guided device driver synthesis
Leonid Ryzhyk, Adam K. Walker, John R. Keys, Alexander Legg, Arun Raghunath, Michael Stumm, Mona Vij · Operating Systems Design and Implementation · 2014
Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. We present the design and implementation of a new driver synthesis toolkit, called Termite-2. Termite-2 is the first tool to combine the power of automation with the flexibility of conventional development. It is also the first practical synthesis tool based on abstraction refinement. Finally, it is the first synthesis tool to support automated debugging of input specifications. We demonstrate the practicality of Termite-2 by synthesizing drivers for a number of I/O devices representative of a typical embedded platform.