ESBMC-Jimple：通过 Jimple 中间表示验证 Kotlin 程序
软件工程
2022-07-21 v2
摘要
在这项工作中，我们描述并评估了首个通过 Jimple 中间表示验证 Kotlin 程序的模型检测器。该验证器名为 ESBMC-Jimple，构建于高效的基于 SMT 的上下文有界模型检测器（ESBMC）之上。它使用 Soot 框架获取 Jimple IR，该 IR 表示 Kotlin 源代码的简化版本，每条指令最多包含三个操作数。ESBMC-Jimple 处理 Kotlin 源代码以及标准 Kotlin 库模型，并检查一组安全属性。实验结果表明，ESBMC-Jimple 能正确验证文献中的一组 Kotlin 基准程序，并且与最先进的 Java 字节码验证器具有竞争力。演示视频可在 https://youtu.be/J6WhNfXvJNc 获取。
引用
@article{arxiv.2206.04397,
title = {ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation},
author = {Rafael Menezes and Daniel Moura and Helena Cavalcante and Rosiane de Freitas and Lucas C. Cordeiro},
journal= {arXiv preprint arXiv:2206.04397},
year = {2022}
}
备注
ACM SIGSOFT International Symposium on Software Testing and Analysis 2022