期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2012
卷号：102
页码：4-17
DOI：10.4204/EPTCS.102.3
出版社：Open Publishing Association
摘要：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.
