References & Citations
Computer Science > Software Engineering
Title: ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation
(Submitted on 9 Jun 2022 (v1), last revised 20 Jul 2022 (this version, v2))
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 this https URL
Submission history
From: Rafael Menezes [view email][v1] Thu, 9 Jun 2022 10:18:53 GMT (2110kb,D)
[v2] Wed, 20 Jul 2022 13:26:30 GMT (2108kb,D)
Link back to: arXiv, form interface, contact.