Thursday, January 13, 2011
Speaker: Leonid Ryzhyk
Venue: IST Austria
Faulty device drivers are the leading source of reliability problems inmodern operating systems. Automatic device driver synthesis aims toaddress this problem by achieving driver correctness by construction.To this end, the driver implementation is generated automatically basedon a formal specification of the device and the interface between thedriver and the operating system.
In this talk I will give a high-level overview of the driver synthesismethodology, present a formalisation of the driver synthesis problem asa controller synthesis problem, and discuss the main challenges thatmust be addressed in order to turn driver synhtesis into a practicaltechnique capable of generating drivers for a wide range of devices.