Dealing with I/O devices in the context of pervasive system verification

Device drivers can be tested and debugged much better with techniques from the field of formal verification than with classical methods. The total verification of drivers together with the underlying hardware, however has remained an unsolved problem. Here we outline a paper-and-pencil solution for this problem and report on the status of the formal verification. This work is part of the Verisoft project. In its subproject 2, the seamless verification of the academic system, comprising hardware, system software and applications, is attempted. We survey the techniques and tools used for program verification in Verisoft.