2nd Linux Driver Verification Workshop 2012

2nd Linux Driver Verification workshop co-located with 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA-2012) that is held 15-18 October 2012 in Amirandes, Heraclion, Crete, Greece.

The goal of the workshop 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 (cf. SV-COMP'12). At the same time, many new issues appear that were not important in previous settings. The LDV workshop provides a forum to discuss specifics of real-world verification of C programs, new issues that appear on the way, and experiences gained. The workshop 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 workshop provides an opportunity to share experience and to establish collaboration between different projects in the domain.

The program of the workshop is as follows:

09:00 - 10:30 Session 1, Chair: D. Beyer
   Linux Device-Drivers Verification Challenges
A. Khoroshilov, V. Mutilin, E. Novikov
   BDD-Based Software Model Checking with CPAchecker
A. Stahlbauer
   Pointer Analysis with Uninterpreted Functions
M. Mandrykin
11:00 - 12:30 Session 2, Chair: A. Petrenko
   Using Aspect-Oriented Programming for Preparing C Programs for Static Verification
E. Novikov
   Conditional Model Checking and Applications to Driver Verification
D. Beyer
   On Our Way to Apply Model Checking on the Kernel
A. Lissy
15:00 - 16:30 Session 3, Chair: A. Khoroshilov
   Coccinelle: Theory and Practice
J. Lawall
   Explicit-Value Analysis based on CEGAR and Interpolation
S. Löwe
   Verification of Linux Device-Driver Code - The unsigned int Case (abstract)
M. Rathgeber, C. Zengler, W. Küchlin
17:00 - 18:30 Session 4, Chairs: D. Beyer and A. Petrenko
   Discussion of Future Directions in Working Groups
   Summary Presentation
   Closing Remarks