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