Научно-исследовательская лаборатория верификации и анализа программ (VorPAL) создана в 2015 году компанией JetBrains и Институтом компьютерных наук и технологий Санкт-Петербургского политехнического университета..

В лаборатории VorPAL студенты, аспиранты и молодые исследователи изучают технологии разработки программного обеспечения на основе формальных методов с применением верификации, статического анализа и трансформации программ.

Текущие проекты

Расширение языка Kotlin

Язык Kotlin является относительно новым языком программирования, который решает некоторые проблемы других языков программирования (Java). В то же время, сам Kotlin также может быть расширен множеством нетривиальных способов.

В нашей лаборатории мы уже исследовали или исследуем в настоящий момент следующие способы расширения языка Kotlin:

• Макросы
• "Жидкие" типы
• Специализация параметризуемых классов
• Реификация типовых параметров классов
• Классы типов
• Сопоставление с образцом
• Вариадические типовые параметры

Concolic тестированиe для языка Kotlin (KEX)

Фаззинг компилятора языка Kotlin (BBF)

Фаззинг является хорошо известным подходом в тестировании, в том числе в применении к компиляторам. Проект Backend Bug Finder (BBF) применяет фаззинг (вместе со множеством других интересных технологий) для поиска сложных и нетривиальных ошибок в компиляторе языка Kotlin.

Инструменты для разработчика

Помимо языка Kotlin, наша лаборатория исследует и другие области разработки ПО, с целью попытаться улучшить жизнь разработчиков. К связанным с этим направлением проектам относятся: ускорение условных точек останова в JVM, добавление поддержки системных вызовов в AFL, межъязыковое применение инструментов анализа при помощи GraalVM.

Предыдущие проекты

Ограниченная проверка моделей

В рамках данного проекта был создан Borealis — инструмент ограниченной проверки моделей для программ на языке C, использующий LLVM и различные SMT-солверы. Из-за нехватки времени и ресурсов в настоящий момент проект приостановлен.

Поиск клонов для IDE

На основе передовых подходов к обнаружению клонов был разработан эффективный инструмент, способный обнаруживать клоны в больших проектах "на лету". После нескольких итераций и улучшений данный инструмент был интегрирован в IntelliJ IDEA и используется в ней для поиска клонов.

Студенческая практика

Наша лаборатория проводит стажировки круглый год, поэтому, если вас заинтересовало то, чем мы занимаемся, вы можете связаться с руководителем лаборатории Владимиром Ицыксоном поадресу vlad@icc.spbstu.ru.