Исследовательская группа

Лаборатория верификации и анализа программ

Borealis (BMC)

Руководители проекта: Марат Ахин, Михаил Беляев
Статус: Активный

UPD: в настоящее время проект приостановлен

Borealis --- это инструмент ограниченной проверки моделей на основе инфраструктуры LLVM, предназначенный для статического анализа программ на языке C. Кроме метода ограниченной проверки моделей, заключающегося в применении современных SAT и SMT солверов для поиска ошибок в программах, Borealis использует и другие подходы к анализу.

Основная цель данного проекта --- узнать границы практической применимости ограниченной проверки моделей на реальных программах, а также возможность ее использования совместно с другими статическими и динамическими анализами.

Участники

Публикации

Дополнительно