2nd Linux Driver Verification Workshop 2012

Второй международный семинар Linux Driver Verification проводится в рамках 5-го международного симпозиума по внедрению формальных методов, верификации и валидации (ISoLA-2012), который состоялся с 15 по 18 октября 2012 года недалеко от г. Ираклион на Крите (Греция). Семинар организуется проф. Дирком Бейером (Университет г. Пассау, Германия) и проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН).

Семинар предоставляет уникальную возможность для обмена опытом между различными командами, занимающимися верификацией модулей ядра ОС Linux, а также для начала более плотного взаимодействия между проектами.

Программа семинара
09:00 - 10:30 1-ое заседание, председатель: проф. Дирк Бейер
   Linux Device-Drivers Verification Challenges
A. Khoroshilov, V. Mutilin, E. Novikov
   BDD-Based Software Model Checking with CPAchecker
A. Stahlbauer
   Pointer Analysis with Uninterpreted Functions
M. Mandrykin
11:00 - 12:30 2-ое заседание, председатель: проф. Александр Петренко
   Using Aspect-Oriented Programming for Preparing C Programs for Static Verification
E. Novikov
   Conditional Model Checking and Applications to Driver Verification
D. Beyer
   On Our Way to Apply Model Checking on the Kernel
A. Lissy
15:00 - 16:30 3-е заседание, председатель: Алексей Хорошилов
   Coccinelle: Theory and Practice
J. Lawall
   Explicit-Value Analysis based on CEGAR and Interpolation
S. Löwe
   Verification of Linux Device-Driver Code - The unsigned int Case (abstract)
M. Rathgeber, C. Zengler, W. Küchlin
17:00 - 18:30 4-ое заседание, председатели: проф. Дирк Бейер и проф. Александр Петренко
   Discussion of Future Directions in Working Groups
   Summary Presentation
   Closing Remarks