Research group

Verification or Program Analysis Lab

Borealis (BMC)

Marat Akhin, Mikhail BelyaevInactive

UPD: currently on hiatus

Borealis is a static analysis system based on the LLVM compiler infrastructure and is mainly built around bounded model checking (BMC) for C. BMC is an efficient technique for sound and complete analysis of bounded programs using SMT or SAT solvers. Borealis employs BMC as the main technique used to detect software defects and contract violations, but is not limited to it.

The main goal of this project is to find the limits of BMC when employed together with other kinds of static (and possibly dynamic) analyses.




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


Azat Abdullin, Daniil Stepanov, Marat Akhin

Read more

Borealis Bounded Model Checker: The Coming of Age Story

September 2017

Marat Akhin, Mikhail Belyaev, Vladimir Itsykson

Read more

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

September 2016

Azat Abdullin, Marat Akhin

Read more

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


M. Belyaev, V. Itsykson

Read more

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


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

Read more

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

Read more

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

December 2015

Marat Akhin, Sam Kolton, Vladimir Itsykson

Read more

Improving Static Analysis by Loop Unrolling on an Arbitrary Iteration


М. Belyaev, М. Akhin, V. Itsykson

Read more

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

December 2014

M. Akhin, M. Belyaev, V. Itsykson

Read more