验证或程序分析实验室
验证或项目分析实验室(又名 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 发送电子邮件。
小组成员







