Новости

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

27.09.2012: Вышла версия 0.4 системы KEDR

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

Наиболее важные изменения в этой версии (подробная информация - в ChangeLog):

02.08.2012: Вышла версия 0.1 альфа 1 системы KernelStrider

KernelStrider даёт возможность собирать данные о работе модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д.

KernelStrider собирает информацию об операциях чтения/записи с памятью, выполняемых анализируемым модулем ядра, а также о вызовах функций и некоторых других событиях. Эти данные можно, в частности, передать для анализа системам, выявляющим "состояния гонки" ("race conditions") в программных компонентах, таким, например, как "offline"-вариант системы ThreadSanitizer, http://code.google.com/p/data-race-test/.

21.06.2012: Linux Driver Verification Workshop в рамках конференции ISoLA 2012

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

23.04.2012: Анонсированы участники Google Summer of Code 2012

Google Open Source Programs Office опубликовал список студенческих проектов, отобранных для участия в программе Google Summer of Code 2012 (GSoC-2012). В рамках этой программы компания Google финансирует работу студентов над различными проектами по разработке свободного программного обеспечения. В этом студентам на добровольных началах помогают менторы из участников, соответствующих проектов.

29.03.2012: Успех BLAST 2.7 на международных соревнованиях по верификации программ

На Первых международных соревнованиях по верификации программ прошедших в рамках конференции TACAS 2012 в Таллине, Эстония разработчикам инструмента статической верификации Си программ BLAST 2.7 была вручена почетная табличка за победу в категории DeviceDrivers64. Также инструмент занял третье место в категории DeviceDrivers. Детальные результаты соревнований можно посмотреть здесь.

24.02.2012: Центр верификации на Embedded World 2012

Центр верификации ОС Linux будет представлен в рамках стенда Open Source Automation Development Lab на выставке Embedded World 2012, которая пройдет с 28 февраля по 1 марта 2012 года в городе Нюрнберг, Германия. Приглашаем всех посетить стенд 341 в павильоне № 5.

Также в рамках параллельно проходящей конференции Алексей Хорошилов представит 1 марта доклад "Опыт применения тяжеловесных инструментов верификации для анализа исходного кода драйверов ОС Linux".

17.02.2012: Совместный семинар Центра верификации и Университета Пассау

С 13 по 17 февраля 2012 года в городе Пассау, Германия, прошел совместный семинар Центра верификации ОС Linux и кафедры программных систем Университета Пассау, посвященный вопросам совместного развития инструмента статической верификации CPAchecker и его использования в проекте верификации драйверов ОС Linux.