14-Apr-2014: 4th Linux Driver Verification Workshop took place in Passau

Submitted by admin on Mon, 14/04/2014 - 07:14

4th Linux Driver Verification Workshop was held in Passau, Germany on April 2-4. The workshop was arranged by prof. Alexander Petrenko (Linux Verification Center, ISPRAS, Moscow, Russia) and prof. Dirk Beyer (University of Passau, Germany).

Philipp Wendler from the University of Passau reported a current status of the CPAchecker project. Peter Häring presented news about VerifierCloud which allows to dramatically reduce time needed for verification. Andreas Holzer described a tool for test generation on the base of CPAchecker, called CPAtiger. Matthias Dangl gave talk "Induction-based Verification" and Stefan Löwe told about "Memory-Graphs". Alexander von Rhein discussed a current status of Software Product Lines verification.

Vadim Mutilin from the Linux Verification Center reported about current achievements in using CPAchecker inside LDV and discussed future plans. Pavel Andrianov presented a static analysis approach to data race detection based on CPAchecker. All the participants, including Mikhail Mandrykin, Alexey Khoroshilov and Ilja Zakharov held discussions devoted to new possibilities in searching for multiple errors during one run of CPAchecker and about other topics of future research.