14.04.2014: В Пассау состоялся четвертый Linux Driver Verification Workshop

Опубликовано admin в Пнд, 14/04/2014 - 06:11

2-4 апреля 2014 года состоялся четвертый международный семинар Linux Driver Verification в Пассау, Германия. Семинар был организован проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН, Москва, Россия) и проф. Дирком Бейером (Dirk Beyer, Университет г. Пассау, Германия).

Филипп Вендлер (Philipp Wendler) из Университета Пассау представил обзор последних достижений и ближайших планов по инструменту CPAchecker. Питер Хэринг (Peter Häring) рассказал о новостях проекта VerifierCloud, позволяющего значительно сократить время, необходимое для верификации. Андреас Хольцер (Andreas Holzer) описал генератор тестов на базе CPAchecker, называемый CPAtiger. Маттиас Дангл (Matthias Dangl) сделал доклад на тему "Induction-based Verification", а Штефан Лёве (Stefan Löwe) рассказал о "Memory-Graphs". Александр фон Рейн (Alexander von Rhein) описал текущее состояние проекта по верификации семейств программных продуктов.

Вадим Мутилин из Центра верификации ОС Linux сообщил о текущих достижениях в использовании CPAchecker в рамках LDV и описал планы на будущее. Павел Андрианов представил доклад о статическом анализе для обнаружения состояний гонок при совместном доступе к данным. Также участники семинара обсудили новые возможности по поиску многих ошибок за один запуск инструмента верификации.