ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation

TL;DR

This paper introduces ESBMC-Jimple, the first model checker for Kotlin programs using Jimple IR, demonstrating its effectiveness and competitiveness with Java verifiers through experimental validation.

Contribution

It presents a novel model checking approach for Kotlin via Jimple IR, integrating with ESBMC and Soot, and evaluates its performance on benchmarks.

Findings

Successfully verifies Kotlin benchmarks

Competitive with Java bytecode verifiers

Effective for safety property checking

Abstract

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.