The University of New South Wales

Automatic verification of message-based device drivers


Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu

Imperial College London



We develop a practical solution to the problem of automatic verification of the interface between device drivers and the OS. Our solution relies on a combination of improved driver architecture and verification tools. It supports drivers written in C and can be implemented in any existing OS, which sets it apart from previous proposals for verification-friendly drivers. Our Linux-based evaluation shows that this methodology amplifies the power of existing verification tools in detecting driver bugs, making it possible to verify properties beyond the reach of traditional techniques.

BibTeX Entry

    month            = nov,
    keywords         = {device drivers, reliability, model checking},
    paperurl         = {},
    booktitle        = {Systems Software Verification},
    author           = {Amani, Sidney and Chubb, Peter and Donaldson, Alastair and Legg, Alexander and Ryzhyk, Leonid and
                        Zhu, Yanjin},
    year             = {2012},
    pages            = {1--14},
    title            = {Automatic Verification of Message-Based Device Drivers},
    address          = {Sydney, Australia}