Новости

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

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

10.03.2014: Центр верификации Linux на Embedded World 2014

Представители нашей команды Вадим Мутилин и Евгений Новиков приняли участие в выставке Embedded World 2014 в рамках стенда Open Source Automation Development Lab. Выставка проходила с 25 по 27 февраля 2014 года в городе Нюрнберг, Германия.

20.02.2014: Выпущен инструментарий LDV Tools 0.5

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

11.10.2013: Выпущен инструментарий LDV Tools 0.4

После более 2-х лет активной разработки был выпущен инструментарий LDV Tools 0.4. Эта версия включает в себя множество улучшений и исправлений ошибок. В целом она состоит из около 900 изменений, которые были сделаны только в репозитории LDV Tools, не включая подмодули. Наиболее существенные изменения следующие:

  • Улучшения существующих спецификаций правил:

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

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

12.05.2013: Проект LDV - первая сотня ошибок в ядре Linux исправлена

С выпуском ядра Linux-3.10-rc1 достигнут первый рубеж для проекта Linux Driver Verification. В этот релиз вошло 100-ое исправление ошибки, обнаруженной в ходе проекта. 86 патчей, подготовленных членами нашей команды, приняты в основную ветку разработки ядра Linux.

15.03.2013: BLAST 2.7.1 на соревнованиях SV-COMP'2013 и результаты экспериментов

BLAST 2.7.1 был представлен на Вторых международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2013. В этом году BLAST завоевал бронзу в категории DeviceDrivers64. Второе место в этой категории занял инструмент CPAchecker, который уже интегрирован в систему верификации Linux Driver Verification. Победителем в категории DeviceDrivers64 стал новый инструмент UFO.

26.02.2013: Вышла версия 0.4.1 системы KEDR

Выпущена версия 0.4.1 системы KEDR, предназначенной для runtime-анализа модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д. Инструменты из состава KEDR работают с модулем ядра, выбранным пользователем. Они позволяют отслеживать вызовы функций данным модулем и сохранять информацию о них в файле ("трасса вызовов"), имитировать нехватку системных ресурсов, выявлять утечки памяти.

В версии 0.4.1 добавлена подержка версий ядра Linux 3.7 и 3.8, а также исправлено несколько проблем.

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

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

07.10.2012: Опубликована программа Linux Driver Verification Workshop

Опубликован предварительный вариант программы Linux Driver Verification Workshop, который пройдёт 15 октября 2012 года в рамках 5-го международного симпозиума по внедрению формальных методов, верификации и валидации (ISoLA-2012).

09:00 - 10:30 Session 1, Chair: D. Beyer
   Linux Device-Drivers Verification Challenges
A. Khoroshilov, V. Mutilin, E. Novikov