Grupo de pesquisa

Laboratório de Análise de Verificação ou Programa

O Laboratório de Verificação ou Análise de Programas (também conhecido como VorPAL) foi cocriado em 2015 pela JetBrains e pelo Instituto de Ciências da Computação e Tecnologias da Universidade Politécnica de São Petersburgo.

No VorPAL, estudantes, pós-graduados e pesquisadores estão desenvolvendo tecnologias de software baseadas em métodos formais, como verificação, análise estática e técnicas de transformação de programas. Esses métodos são usados para melhorar a produtividade do desenvolvedor no dia-a-dia como ferramentas autônomas, extensões de linguagem de programação ou plug-ins de IDE.

Nosso trabalho é quase sempre open source, pois acreditamos sinceramente na pesquisa aberta.

Projetos de pesquisa atuais

Kotlin melhor

O Kotlin é uma linguagem de programação relativamente nova, que resolve vários problemas e deficiências importantes de outras linguagens de programação (Java). Ao mesmo tempo, ela ainda tem muito espaço para melhorias e extensões.

No VorPAL, já exploramos ou estamos explorando as seguintes formas de estender o Kotlin.

  • Macros
  • Tipos líquidos
  • Especialização de classes parametralizadas
  • Genéricos de classe reificados
  • Classes de tipo
  • Correspondência de padrões
  • Genéricos variados

Testes concólicos para Kotlin (KEX)

Testes concólicos (CONCretos + simbÓLICOs) consistem em uma técnica híbrida interessante para testes e verificação de software que combina o melhor das abordagens estática e dinâmica à análise de programas. Nosso projeto, chamado KEX, é uma tentativa de aplicar testes concólicos ao Kotlin.

Fuzzing do compilador Kotlin (BBF)

Fuzzing é uma técnica de teste bem conhecida, que tem um histórico comprovado por ser eficiente em testes de compilador. O Backend Bug Finder (BBF) usa o Fuzzing (e uma infinidade de outras técnicas interessantes) para encontrar bugs não triviais no compilador Kotlin.

Ferramentas de produtividade para desenvolvedores

No VorPAL, nos preocupamos não só com o Kotlin, mas também com todos os outros aspectos relacionados ao desenvolvimento de software. Projetos não relacionados ao Kotlin incluem acelerar pontos de interrupção condicionais na JVM, fazer com que o AFL reconheça chamadas do sistema e tentar aplicar ferramentas entre linguagens via GraalVM.

Projetos de pesquisa anteriores

Verificação de modelos delimitados

Criamos a Borealis, uma ferramenta de verificação de modelos delimitados para a linguagem de programação C e baseada na toolchain LLVM e em vários solvers SMT. Devido à falta de tempo e recursos, este projeto está suspenso.

Detecção de clones para IDEs

Usando abordagens de última geração, implementamos com sucesso uma eficiente ferramenta de detecção de clones online, capaz de analisar grandes bases de código em tempo real. Após várias iterações e muito esforço, essa ferramenta foi transferida e atualmente é usada no IntelliJ IDEA para detecção de clones.

Principais projetos:

A programação simultânea tradicional envolve a manipulação de um estado mutável compartilhado. Os alunos interessados em qualquer uma das nossas áreas de pesquisa são convidados a entrar em contato com o diretor do Laboratório, Vladimir Itsykson, para obter mais informações em vlad@icc.spbstu.ru.

Membros do Grupo

Vladimir Itsykson
Vladimir Itsykson
Gerente de Projetos
Valentyn Sobol
Valentyn Sobol
Pesquisador
Azat Abdullin
Azat Abdullin
Pesquisador
Daniil Stepanov
Daniil Stepanov
Pesquisador
Artyom Aleksyuk
Artyom Aleksyuk
Pesquisador
Marat Akhin
Marat Akhin
Pesquisador
Mikhail Belyaev
Mikhail Belyaev
Pesquisador
Stanislav Ruban
Stanislav Ruban
Estudante