23.06.2013: В Москве состоялся третий Linux Driver Verification Workshop

Опубликовано Vadim Mutilin в СБ, 22/06/2013 - 20:13

Третий семинар Linux Driver Verification прошел в Москве с 19 по 21 июня. Семинар был организован проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН, г. Москва, Россия) и проф. Дирком Бейером (Университет г. Пассау, Германия).

На семинаре Филипп Вендлер (Philipp Wendler) и Штефан Лёве (Stefan Löwe) из Университета Пассау сделали доклад о прошлых, текущих и планируемых работах, касающихся инструмента адаптивного статического анализа [url=http://cpachecker.sosy-lab.org/]CPAchecker[/url], победителя международных соревнований [url=http://sv-comp.sosy-lab.org/2013/results/]SV-COMP 2013[/url]. Андреас Стахлбауер (Andreas Stahlbauer) рассказал о новом подходе к использованию результатов верификации для эффективной регрессионной верфикации, а Питер Хэринг (Peter Häring) представил VerifierCloud - новый инструмент для распределения задач верификации.

Специалисты Центра верификации ОС Linux рассказали о различных аспектах использования иснструментов статического анализа для проверки драйверов ядра ОС Linux. Михаил Мандрыкин рассказал о прототипе анализа указателей в инструменте CPAchecker. Вадим Мутилин доложил про результаты экспериментов с инструментом CPAchecker на различных конфигурациях в применении к драйверам ядра ОС Linux и сделал доклад про методы легковесного статического анализа для обнаружения состояний гонки. Евгений Новиков представил взгляд пользователей на инструменты верификации.