5th Linux Driver Verification Workshop 2015
5th Linux Driver Verification Workshop dedicated to the 10th anniversary of the Linux Verification Center of ISPRAS will be held in Moscow, Russia on September 15-18. The workshop was arranged by prof. Alexander Petrenko (Linux Verification Center, ISPRAS, Moscow, Russia) and prof. Dirk Beyer (University of Passau, Germany).
The workshop provides an opportunity to share experience and to establish collaboration between different projects in the domain.
The preliminary program of the workshop is as follows:
| 09:00 - 15:30 1st day | |
|
Opening Alexey Khoroshilov, Alexander Petrenko |
|
|
Witness Validation and Stepwise Testification Dirk Beyer |
|
|
CPAchecker in LDV Vadim Mutilin |
|
|
Checking several aspects at once Vitaly Mordan |
|
|
Multi-Property Verification Using Precision Control Andreas Stahlbauer |
|
|
Finding Several Bugs at Once Vitaly Mordan |
|
|
BAM: Problems and perspectives Pavel Andrianov |
|
|
Theory-Independent Reuse of Abstraction Formulas: Towards Proof Reuse Karlheinz Friedberger |
|
|
A Web-Interface for the CPAchecker Cloud Sebastian Ott |
|
|
Checking memory safety Anton Vasilyev |
|
| 09:00 - 17:00 2nd day | |
|
Investigating CPAchecker bottlenecks on Linux device drivers Ilya Zakharov |
|
|
Directions for improvements of memory model in CPAchecker Mikhail Mandrykin |
|
|
First Experiments with Complex Specifications Vitaly Mordan |
|
|
K-Induction in CPAchecker Dirk Beyer |
|
| Discussions | |