Forschungsgruppe

Labor für Verifikation oder Programmanalyse

Das Labor für Verifikations- oder Programmanalyse (VorPAL) wurde 2015 von JetBrains und dem Institut für Informatik und Technologien der Polytechnischen Universität St. Petersburg gegründet.

Bei VorPAL entwickeln Studierenden, Postgraduierte und Forschende Softwaretechnologien, die auf formalen Methoden wie Verifizierung, statischer Analyse und Programmtransformationstechniken basieren. Diese Methoden werden verwendet, um die tägliche Entwicklerproduktivität durch eigenständige Tools, Programmiersprachenerweiterungen oder IDE-Plugins zu verbessern.

Unsere Arbeit ist fast immer Open-Source, weil wir von ganzem Herzen an offene Forschung glauben.

Aktuelle Forschungsprojekte

Besseres Kotlin

Kotlin ist eine relativ neue Programmiersprache, die mehrere wichtige Probleme und Schwächen anderer Programmiersprachen (Java) behebt. Gleichzeitig hat es noch viel Raum für Verbesserungen und Erweiterungen.

Bei VorPAL haben wir bereits die folgenden Möglichkeiten zur Erweiterung von Kotlin erforscht oder sind dabei, sie zu erforschen.

  • Makros
  • Liquid-Typen
  • Parametrisierte Klassenspezialisierung
  • Reified-Class-Generics
  • Typklassen
  • Pattern-Matching
  • Variadische Generics

Concolic-Tests für Kotlin (KEX)-

Concolic (CONCrete + symbOLIC)-Testing ist eine interessante Hybridmethode für das Testen und Verifizieren von Software, die das Beste aus statischen und dynamischen Ansätzen zur Programmanalyse kombiniert. Unser Projekt namens KEX ist ein Versuch, Concolic-Testing auf Kotlin anzuwenden.

Kotlin-Compiler-Fuzzing (BBF)

Fuzzing ist eine bekannte Testmethode, die sich bei Compiler-Testing als effizient erwiesen hat. Der Backend Bug Finder (BBF) verwendet Fuzzing (und eine Vielzahl anderer interessanter Methoden), um nicht-triviale Fehler im Kotlin-Compiler zu finden.

Entwickler-Produktivitätstools

Bei VorPAL kümmern wir uns nicht nur um Kotlin, sondern um alles, was mit der Softwareentwicklung zu tun hat. Zu den Projekten, die nicht mit Kotlin zu tun haben, gehören die Beschleunigung von bedingten Breakpoints in der JVM, die Verbesserung der AFL-Systemaufrufe und der Versuch, Tools über GraalVM sprachübergreifend einzusetzen.

Vorherige Forschungsprojekte

Bounded Model Checking

Wir haben ein Bounded-Model-Checking-Tool für die Programmiersprache C namens Borealis entwickelt, das auf der LLVM-Toolchain und verschiedenen SMT-Solvern basiert. Aufgrund des Zeit- und Ressourcenmangels ist dieses Projekt zurzeit auf Eis gelegt.

Klonerkennung für IDEs

Mit modernsten Ansätzen haben wir erfolgreich ein effizientes Online-Klonerkennungstool implementiert, mit dem große Codebasen in Echtzeit analysiert werden können. Nach mehreren Iterationen und viel Aufwand wurde dieses Tool übertragen und wird derzeit in IntelliJ IDEA zur Klonerkennung verwendet.

Hauptprojekte:

Bei der traditionellen gleichzeitigen Programmierung wird ein gemeinsamer veränderbarer Zustand manipuliert. Studierende, die sich für einen unserer Forschungsbereiche interessieren, können sich an den Laborleiter Vladimir Itsykson wenden, um weitere Informationen unter vlad@icc.spbstu.ru zu erhalten.

Gruppenmitglieder

Vladimir Itsykson
Vladimir Itsykson
Projektmanager*in
Valentyn Sobol
Valentyn Sobol
Forscher*in
Azat Abdullin
Azat Abdullin
Forscher*in
Daniil Stepanov
Daniil Stepanov
Forscher*in
Artyom Aleksyuk
Artyom Aleksyuk
Forscher*in
Marat Akhin
Marat Akhin
Forscher*in
Mikhail Belyaev
Mikhail Belyaev
Forscher*in
Stanislav Ruban
Stanislav Ruban
Student*in