21-Jun-2012: Linux Driver Verification Workshop at ISoLA 2012

user warning: Got error 28 from storage engine query: SELECT t.*,v.weight AS v_weight_unused FROM term_node r INNER JOIN term_data t ON r.tid = t.tid INNER JOIN vocabulary v ON t.vid = v.vid WHERE r.vid = 192 ORDER BY v.weight, t.weight, t.name in /opt/drupal-6.33/modules/taxonomy/taxonomy.module on line 640.

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

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.

If you are interested you can submit a paper in ISoLA post-proceedings that will be published by Spinger in the CCIS series (deadline - 15th of October). Otherwise you are welcome to take part in the workshop without publications.