Research group

Verification or Program Analysis Lab

Borealis (BMC)

Project supervisors: Marat Akhin, Mikhail Belyaev
Status: Active

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.