Исследовательская группа

Лаборатория верификации и анализа программ

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

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

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

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

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

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

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

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

Concolic (портмоне от CONCrete + symbOLIC) тестирование — это гибридный подход к тестированию ПО, комбинирующий лучшие элементы статического и динамического анализа. В рамках проекта KEX наша лаборатория пытается применить concolic-тестирование к языку Kotlin.

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

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

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

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

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

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

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

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

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

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

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

Состав

Владимир Ицыксон
Координатор проекта
Азат Абдуллин
Исследователь
Артем Алексюк
Исследователь
Марат Ахин
Исследователь
Михаил Беляев
Исследователь
Валентин Соболь
Исследователь
Даниил Степанов
Исследователь
Марат Динмухаметов
Студент