# ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation

arXiv: https://arxiv.org/abs/2206.04397 · HTML: https://mlsanity.com/paper/2206.04397/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Jun 2022.

## Built on by (most cited first, 1 of 1)

- [How secure is AI-generated Code: A Large-Scale Comparison of Large Language Models](https://mlsanity.com/paper/2404.18353/) (2024)

## Abstract (arXiv)

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.