Trabalho em anais de eventoOpen Access
ESBMC-Jimple: verifying Kotlin programs via jimple intermediate representation
MENEZES, RAFAEL; MOURA, DANIEL; CAVALCANTE, HELENA; DE FREITAS, ROSIANE; CORDEIRO, LUCAS C
Resumo
Resumo
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; it is competitive with state-of-the-art Java bytecode verifiers. A demonstration is available at https://youtu.be/J6WhNfXvJNc.
Autoria
Autores do grupo (1)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
SMT-based model checkingsootsafety propertiesprogram verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento