Verification or Program Analysis Lab
Borealis (BMC)
UPD: currently on hiatus
Borealis is a static analysis system based on 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 out the limits of BMC when employed together with other kinds of static (and possibly dynamic) analysis.
Participants
Materials
Publications
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