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 |