Новости
04.07.2018: Выпущен Klever 1.0
Опубликовано admin в СР, 04/07/2018 - 18:06После нескольких лет работы над принципиально новой версией инструментария для верификации драйверов LDV Tools, мы рады сообщить о выпуске Klever 1.0.
Помимо переработки внутренней архитектуры в Klever реализовано множество новых возможностей:
28.06.2018: Центр верификации Linux на семинаре Sound Static Analysis for Security
Опубликовано admin в ЧТ, 28/06/2018 - 22:2627-28 июня 2018 года на площадке Национального института по стандартизации и технологиям (National Institute of Standards and Technology, NIST) в г.Гейтерсберг (шт. Мэриленд), США, состоялся международный семинар, посвященный применению консервативного статического анализа для обеспечения безопасности программных систем (Sound Static Analysis for Security).
15.06.2018: В Москве пройдет международный семинар CPA&LDV Workshop 2018
Опубликовано Vadim Mutilin в ПТ, 15/06/2018 - 11:56Совместный третий международный семинар по инструменту CPAchecker (CPA) и восьмой семинар по верификации драйверов ОС Linux (LDV) состоится 25-26 сентябре в г.Москва, Россия.
23.04.2018: CPAchecker-BAM-BnB и CPAchecker-BAM-Slicing на SV-COMP'2018
Опубликовано Vadim Mutilin в ВС, 22/04/2018 - 21:00На международных соревнованиях инструментов статической верификации (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
Опубликовано Vadim Mutilin в ЧТ, 07/09/2017 - 18:384-5 сентября 2017 года в Падерборне, Германия состоялся седьмой международный семинар Linux Driver Verification совместно со вторым международным семинаром по инструменту CPAchecker.
28.08.2017: Поиск ошибок, связанных с гонками по данным, в ядре ОС Linux
Опубликовано Vadim Mutilin в Пнд, 28/08/2017 - 12:32Антон Волков закончил проект “Поиск ошибок, связанных с гонками по данным, в ядре ОС Linux”, выполненный в рамках Google Summer of Code 2017 под эгидой The Linux Foundation. Целями проекта были:
- поиск ошибок, связанных с состояниями гонки, в ядре ОС Linux;
- уведомление разработчиков модулей ядра об этих ошибках.
27.08.2017: Поиск ошибок использования памяти в ядре ОС Linux
Опубликовано Vadim Mutilin в ВС, 27/08/2017 - 05:00Антон Васильев закончил проект "Поиск ошибок использования памяти в ядре ОС Linux", выполненный в рамках Google Summer of Code 2017 под эгидой The Linux Foundation. Ошибки использования памяти несут существенные риски для программного обеспечения, но их обнаружение существенно усложняется, если речь идет об операционной системе. Для поиска и отладки таких ошибок в ОС Linux используются специальные сборки ядра ОС.
30.06.2017: В Москве состоялась Международная Ершовская конференция по информатике (PSI-2017)
Опубликовано Vadim Mutilin в ЧТ, 29/06/2017 - 21:00В Москве прошла 11-я Международная Ершовская конференция по информатике (PSI-2017). В рамках данной конференции Евгений Новиков и Илья Захаров, участвующие в проекте Linux Driver Verification, представили доклад, в котором были затронуты проблемы и особенности применения существующих на сегодняшний день инструментов статической верификации к произвольным программам, разрабатываемым на языке Си с расширениями GNU.
30.05.2017: Компонент AstraVer был представлен на международном семинаре Frama-C & SPARK Day 2017
Опубликовано Vadim Mutilin в Пнд, 29/05/2017 - 21:00В презентации на международном семинаре Frama-C & SPARK Day 2017, который состоялся 30 мая в университете Париж Дидро, мы представили наш опыт дедуктивной верификации модулей ядра Linux с помощью платформы Frama-C, Why3 и компонента AstraVer, а также реализованную в нем комбинированную модель ограниченных целых.
27.04.2017: CPAchecker-BAM-BnB и BLAST 2.7.3 на SV-COMP'2017
Опубликовано Vadim Mutilin в СР, 26/04/2017 - 21:00На международных соревнованиях инструментов статической верификации (SV-COMP 2017), проходивших в рамках международной конференции TACAS, Уппсала, Швеция, были представлены доклады по инструментам CPAchecker-BAM-BnB и BLAST 2.7.3.
