Новости

30.06.2017: В Москве состоялась Международная Ершовская конференция по информатике (PSI-2017)

В Москве прошла 11-я Международная Ершовская конференция по информатике (PSI-2017). В рамках данной конференции Евгений Новиков и Илья Захаров, участвующие в проекте Linux Driver Verification, представили доклад, в котором были затронуты проблемы и особенности применения существующих на сегодняшний день инструментов статической верификации к произвольным программам, разрабатываемым на языке Си с расширениями GNU.

30.05.2017: Компонент AstraVer был представлен на международном семинаре Frama-C & SPARK Day 2017

В презентации на международном семинаре Frama-C & SPARK Day 2017, который состоялся 30 мая в университете Париж Дидро, мы представили наш опыт дедуктивной верификации модулей ядра Linux с помощью платформы Frama-C, Why3 и компонента AstraVer, а также реализованную в нем комбинированную модель ограниченных целых.

27.04.2017: CPAchecker-BAM-BnB и BLAST 2.7.3 на SV-COMP'2017

На международных соревнованиях инструментов статической верификации (SV-COMP 2017), проходящей в рамках международной конференции TACAS, Уппсала, Швеция, были представлены доклады по инструментам CPAchecker-BAM-BnB и BLAST 2.7.3.

30.03.2017: Состоялась конференция «РусКрипто’2017»

XIX научно-практическая конференция «РусКрипто’2017», посвященная различным аспектам криптографии, информационной безопасности и защиты информации прошла 21 — 24 марта 2017 года в подмосковном отеле «Солнечный Park Hotel & SPA».

05.03.2017: 3-4 марта состоялась конференция "Инструменты и методы анализа программ 2017" (TMPA-2017)

В Москве 3-4 марта прошла 4-я международная конференция “Методы и инструменты анализа программ” (TMPA-2017), организованная совместно с ACM Sigsoft. В рамках данной конференции представили доклады Павел Андрианов и Илья Захаров, являющиеся участниками проекта Linux Driver Verification.

30.11.2016: Опубликована новая версия Astraver Toolset 1.1

Инструменты Astraver Toolset 1.1 включают в себя следующие улучшения:

Поддержка языка Си

  • Поддержка адресной арифметики с указателями на вложенные структуры, например, макроса `container_of', широкораспространённого в ядре ОС Linux. В частности, теперь появилась возможность доказать корректность указателя на внешнюю структуру, полученного путём вычитания смещения внутренней структуры из указателя на неё.

Новый подход к целочисленным арифметическим операциям в ACSL

27.09.2016: В Пассау состоялся шестой Linux Driver Verification Workshop

22-23 сентября 2016 года в Пассау, Германия состоялся пятый международный семинар Linux Driver Verification совместно с первым международным семинаром по инструменту CPAchecker.

16.08.2016: Анализ потенциальных состояний гонок на ядре ОС Linux

Павел Андрианов закончил проект "Анализ потенциальных состояний гонок на ядре ОС Linux", выполненный в рамках Google Summer of Code 2016 под эгидой The Linux Foundation.

Состояния гонки достаточно сложно обнаружить, так как они проявляют себя только при определённом стечении обстоятельств, и их достаточно трудно исправить, так как они часто требуют переосмысления кода и осторожного выбора примитивов синхронизации.

11.04.2016: BLAST 2.7.3 на SV-COMP'2016

BLAST 2.7.3 был представлен на пятых международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2016 в Эйндховене, Нидерланды. В этом году BLAST выиграл бронзу в категории DeviceDriversLinux64.

BLAST – это классический инструмент статической верификации программ, основанный на предикатных абстракциях и методе CEGAR. Он поддерживается ИСП РАН и активно используется в проекте Linux Driver Verification (LDV).

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

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