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
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.
- 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.
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 email@example.com.
- Vladimir Itsykson Laboratory supervisor
- Azat Abdullin Researcher
- Marat Akhin Researcher
- Artyom Aleksyuk Researcher
- Mikhail Belyaev Researcher
- Valentyn Sobol Researcher
- Daniil Stepanov Researcher
- Alexandr Suhinin Researcher