5th Linux Driver Verification Workshop 2015
Пятый международный семинар Linux Driver Verification по верификации модулей ядра ОС Linux при помощи методов проверки моделей программ (Software Model Checking) состоится 15-16 сентября 2015 года в институте системного программирования (ИСП РАН) в г. Москве. Семинар организуется проф. Дирком Бейером (Университет г. Пассау, Германия) и проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН).
Семинар предоставляет уникальную возможность для обмена опытом между различными командами, занимающимися верификацией модулей ядра ОС Linux, а также для начала более плотного взаимодействия между проектами.
Программа семинара
| 09:00 - 15:30 1-ое заседание 15.09.2015 | |
|
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 2-ое заседание 16.09.2015 | |
|
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 | |