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 | |