5th Linux Driver Verification Workshop 2015

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 = 261 ORDER BY v.weight, t.weight, t.name in /opt/drupal-6.33/modules/taxonomy/taxonomy.module on line 640.

Пятый международный семинар 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