16.10.2012: Состоялся Linux Driver Verification Workshop

Опубликовано admin в Втр, 16/10/2012 - 15:30

15 октября 2012 года в районе г. Ираклион на о. Крит, Греция, прошел семинар Linux Driver Verification, организованный проф. Дирком Бейером (Университет г. Пассау, Германия) и проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН, г. Москва, Россия) в рамках 5-го международного симпозиума по внедрению формальных методов, верификации и валидации ([url=http://www.cs.uni-potsdam.de/isola/isola2012/tracks.html#A15]ISoLA-2012[/url]).

На семинаре Дирк Бейер (Dirk Beyer) и его сотрудники Андреас Стахлбауер (Andreas Stahlbauer) и Стефан Лёве (Stefan Löwe) продемонстрировали последние достижения инструмента адаптивного статического анализа [url=http://cpachecker.sosy-lab.org/]CPAchecker[/url], победителя международных соревнований [url=http://sv-comp.sosy-lab.org/]SV-COMP 2012[/url].

Специалисты Центра верификации ОС Linux рассказали о текущем состоянии проекта верификации драйверов ОС Linux. В докладах Алексея Хорошилова, Евгения Новикова и Михаила Мандрыкина были рассмотрены сложности, возникающие при верификации драйверов, работающих в пространстве ядра операционной системы, и представлены методы по их преодолению.

Юлия Лаваль (Julia Lawall) (INRIA/LIP6, Париж, Франция) представила инструмент Coccinelle, позволяющий применять семантические патчи к исходному коду программ на языке Си. Было наглядным образом продемонстрировано, как Coccinelle используется для поиска ошибок в коде ядра ОС Linux.

Проф. Вольфганг Кучлин (Wolfgang Küchlin) (Университет г. Тюбинген, Германия) рассказал о системе верификации драйверов ОС Linux Avinux и возможностях проверки настраиваемого кода на примере ядра ОС Linux.

Александр Лисси (Alexandre Lissy) из Научно-исследовательской лаборатории информатики Университета г. Тура, Франция, рассказал про способ построения схемы вызываемых функций на основе объектных файлов. С помощью предложенного подхода Александр получил статистику взаимосвязей различных подсистем ядра ОС Linux.

Слайды большинства выступлений доступны на [url=http://linuxtesting.ru/ldv-workshop-2012]странице семинара[/url].