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.
翻译:在这项工作中,我们描述和评价了第一个通过Jimple中间代表机构核查Kotlin方案的模式核对器,名为ESBMC-Jple的核查器建在基于基于SMT的高效环境封闭模型检查器之上。它使用 Soot 框架获取Jimple IR, 代表了每个指示最多包含三个操作的简化版本的Kotlin源代码。ESBMC-Jemple处理Kotlin源代码以及标准Kotlin图书馆的模型,并检查了一套安全性能。实验结果表明,ESBMC-Jpro可以正确核实文献中的一套Kotlin基准,并且它与最新的爪哇副代码核查器具有竞争力。在https://youtu.be/J6WhNfXvJnc上有一个演示。