Research group

Program Analysis and Verification Lab

Borealis

Status: Active

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

Publications

Resources