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

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

Borealis (BMC)

Марат Ахин, Михаил БеляевПриостановлен

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

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

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

Участники

Материалы

Публикации

Distributed Analysis of the BMC Kind: Making It Fit the Tornado Supercomputer

2017

Azat Abdullin, Daniil Stepanov, Marat Akhin

Подробнее

Borealis Bounded Model Checker: The Coming of Age Story

September 2017

Marat Akhin, Mikhail Belyaev, Vladimir Itsykson

Подробнее

By the power of SMT! Mining Function Contracts to Better Bounded Model Checking

September 2016

Azat Abdullin, Marat Akhin

Подробнее

Fast and Safe Concrete Code Execution for Reinforcing Static Analysis and Verification

2015

M. Belyaev, V. Itsykson

Подробнее

Эффективное исполнение программного кода в контролируемом окружении как способ улучшения результатов статического анализа и верификации программ

2015

М.А. Беляев, В.М. Ицыксон

Подробнее

Using a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT Solver

December 2015

M. Petrov, K. Gagarski, M. Belyaev, V. Itsykson

Подробнее

Random Model Sampling: Making Craig Interpolation Work When It Should Not

December 2015

Marat Akhin, Sam Kolton, Vladimir Itsykson

Подробнее

Improving Static Analysis by Loop Unrolling on an Arbitrary Iteration

2014

М. Belyaev, М. Akhin, V. Itsykson

Подробнее

Software Defect Detection by Combining Bounded Model Checking and Approximations of Functions

December 2014

M. Akhin, M. Belyaev, V. Itsykson

Подробнее