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

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

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

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

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

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

Новости