Новости
30.03.2017: Состоялась конференция «РусКрипто’2017»
Опубликовано Vadim Mutilin в СР, 29/03/2017 - 21:00XIX научно-практическая конференция «РусКрипто’2017», посвященная различным аспектам криптографии, информационной безопасности и защиты информации прошла 21 — 24 марта 2017 года в подмосковном отеле «Солнечный Park Hotel & SPA».
05.03.2017: 3-4 марта состоялась конференция "Инструменты и методы анализа программ 2017" (TMPA-2017)
Опубликовано Vadim Mutilin в СБ, 04/03/2017 - 21:00В Москве 3-4 марта прошла 4-я международная конференция “Методы и инструменты анализа программ” (TMPA-2017), организованная совместно с ACM Sigsoft. В рамках данной конференции представили доклады Павел Андрианов и Илья Захаров, являющиеся участниками проекта Linux Driver Verification.
30.11.2016: Опубликована новая версия Astraver Toolset 1.1
Опубликовано admin в СР, 30/11/2016 - 18:49Инструменты Astraver Toolset 1.1 включают в себя следующие улучшения:
Поддержка языка Си
- Поддержка адресной арифметики с указателями на вложенные структуры, например, макроса `container_of', широкораспространённого в ядре ОС Linux. В частности, теперь появилась возможность доказать корректность указателя на внешнюю структуру, полученного путём вычитания смещения внутренней структуры из указателя на неё.
Новый подход к целочисленным арифметическим операциям в ACSL
27.09.2016: В Пассау состоялся шестой Linux Driver Verification Workshop
Опубликовано Vadim Mutilin в Пнд, 26/09/2016 - 21:0022-23 сентября 2016 года в Пассау, Германия состоялся шестой международный семинар Linux Driver Verification совместно с первым международным семинаром по инструменту CPAchecker.
16.08.2016: Анализ потенциальных состояний гонок на ядре ОС Linux
Опубликовано admin в Втр, 16/08/2016 - 07:17Павел Андрианов закончил проект "Анализ потенциальных состояний гонок на ядре ОС Linux", выполненный в рамках Google Summer of Code 2016 под эгидой The Linux Foundation.
Состояния гонки достаточно сложно обнаружить, так как они проявляют себя только при определённом стечении обстоятельств, и их достаточно трудно исправить, так как они часто требуют переосмысления кода и осторожного выбора примитивов синхронизации.
11.04.2016: BLAST 2.7.3 на SV-COMP'2016
Опубликовано Vadim Mutilin в Пнд, 11/04/2016 - 16:10BLAST 2.7.3 был представлен на пятых международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2016 в Эйндховене, Нидерланды. В этом году BLAST выиграл бронзу в категории DeviceDriversLinux64.
BLAST – это классический инструмент статической верификации программ, основанный на предикатных абстракциях и методе CEGAR. Он поддерживается ИСП РАН и активно используется в проекте Linux Driver Verification (LDV).
13.10.2015: Проект LDV - исправлена вторая сотня ошибок в ядре Linux
Опубликовано Vadim Mutilin в Пнд, 12/10/2015 - 21:00С выпуском ядра Linux-4.3-rc1 достигнут второй рубеж для проекта Linux Driver Verification. В этот релиз вошло 200 исправлений ошибок, обнаруженных в ходе проекта. 151 патч, подготовленный членами нашей команды, принят в основную ветку разработки ядра Linux.
02.10.2015: 10 лет Центра верификации ОС Linux.
Опубликовано Vadim Mutilin в ЧТ, 01/10/2015 - 21:0022 октября 2015 года в 18.00 в Цетре Digital October в рамках конференции "Разработка ПО" CEE-SEC(R) состоится круглый стол "10 лет Центра верификации ОС Linux. Верификация реального ПО – мечта или реальность?"
23.09.2015: В Москве состоялся пятый Linux Driver Verification Workshop
Опубликовано Vadim Mutilin в Втр, 22/09/2015 - 21:0015-18 сентября 2015 года в Москве состоялся пятый международный семинар Linux Driver Verification посвященный десятой годовщине Центра Верификации ОС Linux. Семинар был организован проф. Александром Петренко (Центр верификации ОС Linux, ИСП РАН, Москва, Россия) и проф. Дирком Бейером (Dirk Beyer, Университет г. Пассау, Германия).
13.05.2015: Выпущен инструментарий LDV Tools 0.8
Опубликовано Vadim Mutilin в СР, 13/05/2015 - 07:57Наиболее важные изменения, которые вошли в LDV Tools 0.8:
- Инструмент верификации CPAchecker обновлен до новой версии 1.4 (r14998).
- Инструментарий LDV Tools теперь доступен в виде контейнеров платформы виртуализации Docker, благодаря этому, теперь не требуется установка всех зависимостей на ваш компьютер.
- Улучшения в 13 существующих спецификациях правил: