Новости

13.08.2018: Улучшение модели окружения для задач верификации ядра ОС Linux на корректность использования памяти и поиск ошибок использования памяти в ядре ОС Linux

Антон Васильев закончил проект "Улучшение модели окружения для задач верификации ядра ОС Linux на корректность использования памяти и поиск ошибок использования памяти в ядре ОС Linux", выполненный в рамках Google Summer of Code 2018 под эгидой The Linux Foundation.

04.07.2018: Выпущен Klever 1.0

После нескольких лет работы над принципиально новой версией инструментария для верификации драйверов LDV Tools, мы рады сообщить о выпуске Klever 1.0.

Помимо переработки внутренней архитектуры в Klever реализовано множество новых возможностей:

28.06.2018: Центр верификации Linux на семинаре Sound Static Analysis for Security

27-28 июня 2018 года на площадке Национального института по стандартизации и технологиям (National Institute of Standards and Technology, NIST) в г.Гейтерсберг (шт. Мэриленд), США, состоялся международный семинар, посвященный применению консервативного статического анализа для обеспечения безопасности программных систем (Sound Static Analysis for Security).

15.06.2018: В Москве пройдет международный семинар CPA&LDV Workshop 2018

Совместный третий международный семинар по инструменту CPAchecker (CPA) и восьмой семинар по верификации драйверов ОС Linux (LDV) состоится 25-26 сентябре в г.Москва, Россия.

23.04.2018: CPAchecker-BAM-BnB и CPAchecker-BAM-Slicing на SV-COMP'2018

На международных соревнованиях инструментов статической верификации (SV-COMP 2018), проходивших в рамках международной конференции TACAS, Салоники, Греция, были представлены доклады по инструментам CPAchecker-BAM-BnB и CPAchecker-BAM-Slicing. В этом году наш инструмент CPAchecker-BAM-BnB завоевал золотую медаль, а CPAchecker-BAM-Slicing завоевал бронзовую медаль в категории Software Systems.

07.09.2017: В Падерборне состоялся седьмой Linux Driver Verification Workshop

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

28.08.2017: Поиск ошибок, связанных с гонками по данным, в ядре ОС Linux

Антон Волков закончил проект “Поиск ошибок, связанных с гонками по данным, в ядре ОС Linux”, выполненный в рамках Google Summer of Code 2017 под эгидой The Linux Foundation. Целями проекта были:

  1. поиск ошибок, связанных с состояниями гонки, в ядре ОС Linux;
  2. уведомление разработчиков модулей ядра об этих ошибках.

27.08.2017: Поиск ошибок использования памяти в ядре ОС Linux

Антон Васильев закончил проект "Поиск ошибок использования памяти в ядре ОС Linux", выполненный в рамках Google Summer of Code 2017 под эгидой The Linux Foundation. Ошибки использования памяти несут существенные риски для программного обеспечения, но их обнаружение существенно усложняется, если речь идет об операционной системе. Для поиска и отладки таких ошибок в ОС Linux используются специальные сборки ядра ОС.

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, а также реализованную в нем комбинированную модель ограниченных целых.