Laboratoire de vérification ou d’analyse de programme

Le Laboratoire de vérification ou d’analyse de programme (alias VorPAL) a été créé en 2015 par JetBrains et l’Institut des sciences et technologies informatiques de l’Université polytechnique de Saint-Pétersbourg.

À VorPAL, les étudiants, les étudiants de troisième cycle et les chercheurs développent des technologies logicielles basées sur des méthodes formelles, telles que la vérification, l’analyse statique et les techniques de transformation des programmes. Ces méthodes sont utilisées pour améliorer la productivité quotidienne des développeurs sous forme qu’outils autonomes, d'extensions de langage de programmation ou de plugins IDE.

Notre travail est presque toujours open-source parce que nous croyons de tout cœur en la recherche ouverte.

Projets de recherche actuels

Amélioration de Kotlin

Kotlin est un langage de programmation relativement nouveau, qui résout plusieurs problèmes importants et lacunes d’autres langages de programmation (Java). Néanmoins, il a encore beaucoup de possibilités d'amélioration et d'extension.

À VorPAL, nous avons déjà exploré ou explorons actuellement les moyens suivants d’étendre Kotlin.

• Macros
• Types liquides
• Spécialisation de classe paramétrisée
• Génériques de classe Reified
• Classes de type
• Reconnaissance de schémas
• Génériques variadiques

Tests concoliques pour Kotlin (KEX)

Le test concolique (CONCrete + symbOLIQUE) est une technique hybride intéressante pour les tests logiciels et la vérification, qui combine le meilleur des approches statiques et dynamiques à l’analyse du programme. Notre projet appelé KEX est une tentative d’appliquer des tests concoliques à Kotlin.

Fuzzing du compilateur Kotlin (BBF)

Le fuzzing est une technique de test bien connue, qui a fait ses preuves en termes d’efficacité dans les tests de compilateur. Backend Bug Finder (BBF) utilise le fuzzing (et une pléthore d’autres techniques intéressantes) pour trouver des bugs non triviaux dans le compilateur Kotlin.

Outils de productivité pour développeurs

À VorPAL, nous nous soucions non seulement de Kotlin, mais aussi de tout ce qui concerne le développement de logiciels. Les projets non liés à Kotlin comprennent l'accélération des points d'arrêt conditionnels dans la JVM, la prise de conscience des appels du système AFL et la tentative d’appliquer des outils de façon transversale via GraalVM.

Projets de recherche passés

Vérification de modèle délimité

Nous avons créé un outil de vérification de modèle délimité pour le langage de programmation C appelé Borealis, basé sur la boîte à outils LLVM et divers solveurs SMT. En raison du manque de temps et de ressources, ce projet est en pause.

Détection de clones pour les IDE

En utilisant des approches de pointe, nous avons mis en œuvre avec succès un outil efficace de détection en ligne de clones, capable d’analyser de grandes bases de code en temps réel. Après plusieurs itérations et beaucoup d’efforts, cet outil a été transféré et est actuellement utilisé dans IntelliJ IDEA pour la détection de clones.

Principaux projets :

La programmation concurrente traditionnelle implique la manipulation d'un état mutable partagé. Les étudiants qui sont intéressés par l’un de nos domaines de recherche sont invités à contacter le directeur du laboratoire Vladimir Itsykson pour plus d’informations à vlad@icc.spbstu.ru.