Research group

Program Analysis and Verification Lab

The Program Analysis and Verification Lab (aka Verification or Program Analysis Lab aka VorPAL) was co-established in 2015 by JetBrains and the Institute of Computer Sciences and Technologies of the St. Petersburg Polytechnic University.

At VorPAL, students, postgraduates, and researchers are developing software technologies based on formal methods, such as verification, static analysis, and program transformation techniques. These methods are used to improve day-to-day developer productivity as standalone tools, programming language extensions or IDE plugins.

Our work is almost always open-source, because we wholeheartedly believe in open research.

Current research projects

Better Kotlin

Kotlin is a relatively new programming language, which solves several important problems and short-comings of other programming languages (Java). At the same time, it still has a lot of room for improvements and extensions.

At VorPAL, we have already explored or are currently exploring the following ways of extending Kotlin.

  • Macros
  • Liquid types
  • Parameterized class specialization
  • Reified class generics
  • Type classes
  • Pattern matching
  • Variadic generics

Concolic testing for Kotlin (KEX)

Concolic (CONCrete + symbOLIC) testing is an interesting hybrid technique for software testing and verification, which combines the best parts of static and dynamic approaches to program analysis. Our project called KEX is an attempt to apply concolic testing to Kotlin.

Kotlin compiler fuzzing (BBF)

Fuzzing is a well-known testing technique, which has a proven history of being efficient in compiler testing. Backend Bug Finder (BBF) uses fuzzing (and a plethora of other interesting techniques) to find non-trivial bugs in Kotlin compiler.

Developer productivity tools

At VorPAL, we care not only for Kotlin, but for all things related to software development. Non-Kotlin-related projects include speeding up conditional breakpoints in JVM, making AFL system-call-aware and attempting to apply tools in a cross-language fashion via GraalVM.

Previous research projects

Bounded model checking

We have created a bounded model checking tool for C programming language called Borealis, based on the LLVM toolchain and various SMT solvers. Due to the lack of time and resources, this project is on hiatus.

Clone detection for IDEs

Using state-of-the-art approaches, we successfully implemented an efficient online clone detection tool, able to analyze large code bases in real time. After several iterations and a lot of effort, this tool has been transferred and is currently used in IntelliJ IDEA for clone detection.

Student Internship

We are hiring interns all year round, so students who are interested in any of our research areas are welcome to contact the Lab Director Vladimir Itsykson for more information at vlad@icc.spbstu.ru.

News