Linux Driver Verification Workshop
The goal of the track on Linux driver verification is to bring together researchers and practitioners that work in the area of functional, safety, and security verification of real-life software written in C. The research in program analysis, SMT solvers, model checking, and other areas of software verification has made a significant progress in terms of precision and performance. State-of-the-art verification tools have become applicable to real-life software such as device drivers. At the same time, many new issues appear that were not important in previous settings. The LDV track provides a forum to discuss specifics of real-world verification of C programs, new issues that appear on the way, and experiences gained. The track is devoted to Linux device-driver verification, because the Linux kernel-space code is different from usual C programs in several aspects. At the same time, this code base is a very popular target for many research projects for various reasons.
The track provides an opportunity to share experience and to establish collaboration between different projects in the domain.
More information can be found here.