一句话：提出首个基于 Jimple 中间表示的 Kotlin 程序模型检测器 ESBMC-Jimple，并验证其竞争力。
本文针对 Kotlin 程序缺乏专用模型检测工具的问题，提出并实现首个通过 Jimple 中间表示进行验证的模型检测器 ESBMC-Jimple。该工具构建于基于 SMT 的有界上下文模型检测器 ESBMC 之上，利用 Soot 框架将 Kotlin 源码转换为每指令至多三个操作数的简化 Jimple IR，并结合标准 Kotlin 库模型对源码检查一组安全属性。实验使用文献中的 Kotlin 基准，结果显示 ESBMC-Jimple 能正确验证这些程序，且与最先进的 Java 字节码验证器相比具有竞争力。作者还提供了演示视频。
We describe and evaluate the first model checker for verifying Kotlin programs through the Jimple intermediate representation. The verifier, named ESBMC-Jimple, is built on top of the Efficient SMT-based Context-Bounded Model Checker (ESBMC). It uses the Soot framework to obtain the Jimple IR, representing a simplified version of the Kotlin source code, containing a maximum of three operands per instruction. ESBMC-Jimple processes Kotlin source code together with a model of the standard Kotlin libraries and checks a set of safety properties. Experimental results show that ESBMC-Jimple can correctly verify a set of Kotlin benchmarks from the literature; it is competitive with state-of-the-art Java bytecode verifiers. A demonstration is available at https://youtu.be/J6WhNfXvJNc.
@inproceedings{paperbot7406,
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},
booktitle = {ISSTA},
year = {2022},
doi = {10.1145/3533767.3543294}
}