论文标题
ESBMC-Jimple：通过Jimple中间表示验证Kotlin程序
ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation
论文作者
论文摘要
在这项工作中，我们描述并评估了第一个模型检查器，用于通过Jimple中间表示验证Kotlin程序。该验证者名为ESBMC-JIMPLE，是在有效的基于SMT的上下文结合模型检查器（ESBMC）的顶部构建的。它使用烟灰框架获取Jimple IR，代表了Kotlin源代码的简化版本，每个说明最多包含三个操作数。 ESBMC-Jimple处理Kotlin源代码以及标准Kotlin库的模型，并检查一组安全属性。实验结果表明，ESBMC-JIMPLE可以正确验证文献中的一组Kotlin基准，并且它与最新的Java字节码验证符具有竞争力。可以在https://youtu.be/j6whnfxvjnc上获得演示。
In this work, 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 and that it is competitive with state-of-the-art Java bytecode verifiers. A demonstration is available at https://youtu.be/J6WhNfXvJNc.
