16-Oct-2012: Linux Driver Verification Workshop took place

Linux Driver Verification workshop was held near the city Heraklion (Crete, Greece) at October 15. The workshop was arranged by prof. Dirk Beyer (University of Passau, Germany) and prof. Alexander Petrenko (Linux Verification Center, ISPRAS, Moscow, Russia) within 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ([url=http://www.cs.uni-potsdam.de/isola/isola2012/tracks.html#A15]ISoLA-2012[/url]).

Dirk Beyer, Andreas Stahlbauer and Stefan Löwe from University of Passau presented recent developments of the configurable software verification platform [url=http://cpachecker.sosy-lab.org/]CPAchecker[/url], that has won the international competition [url=http://sv-comp.sosy-lab.org/]SV-COMP 2012[/url].

Linux Verification Center team reported a current state of the Linux Driver Verification project. Alexey Khoroshilov, Evgeny Novikov and Mikhail Mandrykin cover topics of challenges arising from application of verification tools to kernel space device drivers and approaches to meet them.

Julia Lawall from INRIA/LIP6 (Paris, France) presented Coccinelle. This tool is intended to apply semantics patches to C programs source code. Julia demonstrated how one can use Coccinelle for finding bugs in Linux kernel.

Prof. Wolfgang Küchlin from University of Tübingen (Germany) told about the Linux driver verification framework Avinux. Also he presented a recent research work concerned with a product-line simulation. Wolfgang considered the Linux kernel as an example of product-line code.

Alexandre Lissy from the Laboratory of Computer Science (University of Tours, France) told about obtaining call graph on the basis of object files. Using this approach Alexandre has calculated a statistics of Linux kernel subsystem interrelations.

Most slides are available at the [url=http://linuxtesting.org/ldv-workshop-2012]event homepage[/url].