Grupo de investigación

Laboratorio de Verificación o Análisis de Programas

El Laboratorio de Verificación o Análisis de Programas (también conocido como VorPAL) nació en 2015 de manos de JetBrains y el Institute of Computer Sciences and Technologies de la Universidad Politécnica de San Petersburgo.

En el VorPAL, estudiantes, graduados e investigadores desarrollan tecnologías de software basadas en métodos formales, como la verificación, el análisis estático y las técnicas de transformación de programas. Estos métodos se utilizan para mejorar la productividad diaria de los desarrolladores como herramientas independientes, extensiones de lenguaje de programación o complementos del IDE.

Nuestro trabajo es casi siempre de código abierto porque creemos firmemente en la investigación abierta.

Proyectos de investigación actuales

Mejor Kotlin

Kotlin es un lenguaje de programación relativamente nuevo, que resuelve varios problemas importantes y deficiencias graves de otros lenguajes de programación (Java). Al mismo tiempo, todavía tiene mucho margen de mejora y posibles extensiones.

En el VorPAL, ya hemos explorado o estamos explorando las siguientes formas de ampliar Kotlin.

  • Macros
  • Tipos líquidos
  • Especialización de clase parametrizada
  • Genéricos de clase reificados
  • Clases de tipo
  • Coincidencia de patrones
  • Genéricos variádicos

Pruebas Concolic para Kotlin (KEX)

Las pruebas Concolic (CONCrete + symbOLIC) son una interesante técnica híbrida para realizar pruebas y verificaciones de software, que combinan lo mejor de los enfoques estáticos y los dinámicos para el análisis de programas. Nuestro proyecto, llamado KEX, es un intento de realizar pruebas Concolic con Kotlin.

Pruebas de vulnerabilidad ante datos aleatorios del compilador de Kotlin (BBF)

El fuzzing o pruebas de vulnerabilidad ante datos aleatorios es una conocida técnica de prueba, que ha demostrado ser eficiente en las pruebas del compilador. El Backend Bug Finder (BBF) utiliza el fuzzing (y muchas otras técnicas interesantes) para encontrar errores no triviales en el compilador de Kotlin.

Herramientas de productividad para desarrolladores

En el VorPAL, nos solo nos preocupamos por Kotlin, sino por todo lo relacionado con el desarrollo de software. Los proyectos no relacionados con Kotlin incluyen acelerar los puntos de interrupción condicionales de la JVM, hacer que el AFL sea consciente de las llamadas del sistema e intentar aplicar herramientas entre lenguajes con GraalVM.

Proyectos de investigación anteriores

Comprobación de modelos limitados

Hemos creado una herramienta de comprobación de modelos limitadas para el lenguaje de programación C llamado Borealis, basada en la cadena de herramientas LLVM y varios solucionadores SMT. Debido a la falta de tiempo y recursos, este proyecto está en pausa.

Detección de clones para el IDE

Con enfoques de última generación, implementamos con éxito una herramienta eficiente de detección de clones en línea, capaz de analizar grandes bases de código en tiempo real. Después de varias iteraciones y mucho esfuerzo, esta herramienta se ha transferido y se utiliza actualmente en IntelliJ IDEA para la detección de clones.

Proyectos principales:

La programación simultánea tradicional incluye la manipulación de un estado mutable compartido. Los estudiantes que estén interesados en cualquiera de nuestras áreas de investigación pueden ponerse en contacto con el director del laboratorio Vladimir Itsykson para obtener más información a través del correo vlad@icc.spbstu.ru.

Miembros del grupo

Vladimir Itsykson
Vladimir Itsykson
Gestor de proyectos
Valentyn Sobol
Valentyn Sobol
Investigador
Azat Abdullin
Azat Abdullin
Investigador
Daniil Stepanov
Daniil Stepanov
Investigador
Artyom Aleksyuk
Artyom Aleksyuk
Investigador
Marat Akhin
Marat Akhin
Investigador
Mikhail Belyaev
Mikhail Belyaev
Investigador
Stanislav Ruban
Stanislav Ruban
Estudiante