验证或程序分析实验室

验证或项目分析实验室（又名 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 发送电子邮件。