Новости
11.10.2013: Выпущен инструментарий LDV Tools 0.4
Опубликовано admin в ПТ, 11/10/2013 - 12:44После более 2-х лет активной разработки был выпущен инструментарий LDV Tools 0.4. Эта версия включает в себя множество улучшений и исправлений ошибок. В целом она состоит из около 900 изменений, которые были сделаны только в репозитории LDV Tools, не включая подмодули. Наиболее существенные изменения следующие:
- Улучшения существующих спецификаций правил:
23.06.2013: В Москве состоялся третий Linux Driver Verification Workshop
Опубликовано Vadim Mutilin в СБ, 22/06/2013 - 20:13Третий семинар Linux Driver Verification прошел в Москве с 19 по 21 июня. Семинар был организован проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН, г. Москва, Россия) и проф. Дирком Бейером (Университет г. Пассау, Германия).
12.05.2013: Проект LDV - первая сотня ошибок в ядре Linux исправлена
Опубликовано admin в ВС, 12/05/2013 - 05:04С выпуском ядра Linux-3.10-rc1 достигнут первый рубеж для проекта Linux Driver Verification. В этот релиз вошло 100-ое исправление ошибки, обнаруженной в ходе проекта. 86 патчей, подготовленных членами нашей команды, приняты в основную ветку разработки ядра Linux.
15.03.2013: BLAST 2.7.1 на соревнованиях SV-COMP'2013 и результаты экспериментов
Опубликовано admin в СБ, 16/03/2013 - 18:06BLAST 2.7.1 был представлен на Вторых международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2013. В этом году BLAST завоевал бронзу в категории DeviceDrivers64. Второе место в этой категории занял инструмент CPAchecker, который уже интегрирован в систему верификации Linux Driver Verification. Победителем в категории DeviceDrivers64 стал новый инструмент UFO.
26.02.2013: Вышла версия 0.4.1 системы KEDR
Опубликовано admin в Пнд, 04/03/2013 - 03:42Выпущена версия 0.4.1 системы KEDR, предназначенной для runtime-анализа модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д. Инструменты из состава KEDR работают с модулем ядра, выбранным пользователем. Они позволяют отслеживать вызовы функций данным модулем и сохранять информацию о них в файле ("трасса вызовов"), имитировать нехватку системных ресурсов, выявлять утечки памяти.
В версии 0.4.1 добавлена подержка версий ядра Linux 3.7 и 3.8, а также исправлено несколько проблем.
16.10.2012: Состоялся Linux Driver Verification Workshop
Опубликовано admin в Втр, 16/10/2012 - 15:3015 октября 2012 года в районе г. Ираклион на о. Крит, Греция, прошел семинар Linux Driver Verification, организованный проф. Дирком Бейером (Университет г. Пассау, Германия) и проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН, г. Москва, Россия) в рамках 5-го международного симпозиума по внедрению формальных методов, верификации и валидации ([url=http://www.cs.uni-potsdam.de/isola/isola2012/tracks.html#A15]ISoLA-2012[/url]).
07.10.2012: Опубликована программа Linux Driver Verification Workshop
Опубликовано admin в ВС, 07/10/2012 - 20:40Опубликован предварительный вариант программы 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
Опубликовано admin в ЧТ, 27/09/2012 - 20:37Выпущена версия 0.4 системы KEDR, предназначенной для runtime-анализа модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д. Инструменты из состава KEDR работают с модулем ядра, выбранным пользователем. Они позволяют отслеживать вызовы функций данным модулем и сохранять информацию о них в файле ("трасса вызовов"), имитировать нехватку системных ресурсов, выявлять утечки памяти.
Наиболее важные изменения в этой версии (подробная информация - в ChangeLog):
02.08.2012: Вышла версия 0.1 альфа 1 системы KernelStrider
Опубликовано admin в ЧТ, 02/08/2012 - 17:21KernelStrider даёт возможность собирать данные о работе модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д.
KernelStrider собирает информацию об операциях чтения/записи с памятью, выполняемых анализируемым модулем ядра, а также о вызовах функций и некоторых других событиях. Эти данные можно, в частности, передать для анализа системам, выявляющим "состояния гонки" ("race conditions") в программных компонентах, таким, например, как "offline"-вариант системы ThreadSanitizer, http://code.google.com/p/data-race-test/.
21.06.2012: Linux Driver Verification Workshop в рамках конференции ISoLA 2012
Опубликовано admin в ЧТ, 21/06/2012 - 06:09Мы рады сообщить о проведении Linux Driver Verification Workshop в рамках 5-го международного симпозиума по внедрению формальных методов, верификации и валидации (ISoLA-2012), который пройдет с 15 по 18 октября 2012 года недалеко от г. Ираклион на Крите (Греция). Семинар организуется проф. Дирком Бейером (Университет г. Пассау, Германия) и проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН).