Research group

Program Analysis and Verification Lab

The Program Analysis and Verification Lab was established in 2015 by JetBrains and the Institute of Computer Sciences and Technologies of the St. Petersburg Polytechnic University. At the laboratory, students, postgraduates, and developers are researching software technologies based on formal methods. Also, they're developing some useful tools utilizing verification, static analysis and program transformation techniques.

Currently, there are four projects in development at the Lab:

Program verification and error detection through Bounded Model Checking. The goal of this project is to create tools for detecting errors and “violations of contract” in software with bounded model checking (BMC) and SMT solvers.

Real-time clone detection. An interactive tool, which is currently being developed at the Lab, will be able to identify duplication in the source code automatically. This instrument is planned to be fully integrated with IntelliJ IDEA.

Automated bug fixing. The idea is to create a tool that can automatically fix some of the errors detected by static code analysis.

Co-design solution based on Kotlin. The Lab is developing a new technology for cooperative software-hardware designing, which is based on Kotlin (statically typed programming language created at JetBrains). This solution is intended to replace currently available co-design systems, which utilize cumbersome and inconvenient SystemC language.

Students who are interested in any of those subjects are welcomed to contact the Lab Director Vladimir Mikhailovich