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

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

Научно-исследовательская лаборатория верификации и анализа программ (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.

Состав

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