研究小组

验证或程序分析实验室

验证或项目分析实验室(又名 VorPAL)由 JetBrains 和圣彼得堡理工大学计算机科学与技术学院于 2015 年共同建立。

在 VorPAL,学生、研究生和研究人员正在开发基于正式方法的软件技术,如验证、静态分析和程序转换技术。 这些方法用于提高开发人员作为独立工具、编程语言扩展或 IDE 插件的工作效率。

我们的工作几乎都是开源的,因为我们全心全意地相信开放的研究工作。

目前正在进行的研究项目

更好的 Kotlin

Kotlin 是一种相对较新的编程语言,它解决了其他编程语言(Java)的一些重要问题和缺点。 同时,它仍有很多改进和扩展的余地。

在 VorPAL,我们已经探索或目前正在探索以下方法来扩展 Kotlin。

  • Liquid 类型
  • 参数化类专用化
  • 具体化类泛型
  • 类型类
  • 模式匹配
  • Variadic 泛型

Kotlin 的 Concolic 测试(KEX)

Concolic (CONCrete + symbOLIC, 具体和符号) 测试是一种有趣的软件测试和验证混合技术,它结合了最佳的静态和动态程序分析方法。 我们的项目称为 KEX, 是尝试对 Kotlin 应用 Conclic 测试。

Kotlin 编译器模糊 (BBF)

模糊测试是一种众所周知的测试技术,它具有在编译器测试中高效运行的悠久历史。 Backend Bug Finder (BBF) 使用模糊测试(以及大量其他有趣的技术)在 Kotlin 编译器中查找非平凡的错误。

开发人员的高效工具

在 VorPAL,我们不仅对 Kotlin 感兴趣,也关注所有与软件开发相关的事情。 与 Kotlin 无关的项目包括加快 JVM 中的条件断点、使AFL具有系统调用意识,以及尝试通过 GraalVM 以跨语言方式应用工具。

以前的研究项目

边界模型检查

我们为 C 编程语言创建了一个称为 Borealis 的边界模型检查工具,基于 LLVM 工具链和各种 SMT 解算器。 由于缺乏时间和资源,这个项目处于停顿状态。

IDE 克隆检测

使用最先进的方法,我们成功实现了高效的在线克隆检测工具,能够实时分析大型代码库。 经过多次的迭代和大量的努力,这个工具已经被转移到了IntelliJ IDEA中,并被用于克隆检测。

主要项目:

传统的并发编程涉及到对共享的可变状态进行操作。 欢迎对我们任何研究领域感兴趣的学生与实验室主任 Vladimir Itsykson 联系,以了解更多信息。 请向 vlad@icc.spbstu.ru 发送电子邮件。

小组成员

Vladimir Itsykson
Vladimir Itsykson
项目经理
Valentyn Sobol
Valentyn Sobol
研究员
Azat Abdullin
Azat Abdullin
研究员
Daniil Stepanov
Daniil Stepanov
研究员
Artyom Aleksyuk
Artyom Aleksyuk
研究员
Marat Akhin
Marat Akhin
研究员
Mikhail Belyaev
Mikhail Belyaev
研究员
Stanislav Ruban
Stanislav Ruban
学生