ISSTA 2022 (series) / Tool Demonstrations /
ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation
Thu 21 Jul 2022 10:16 - 10:21 at Tool demo - Tool Demonstrations
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 .
Thu 21 JulDisplayed time zone: Seoul change
Thu 21 Jul
Displayed time zone: Seoul change
10:00 - 11:00 | |||
10:00 5mTalk | ATUA: an Update-driven App Testing Tool Tool Demonstrations Chanh-Duc Ngo University of Luxembourg, Fabrizio Pastore University of Luxembourg, Lionel Briand University of Luxembourg; University of Ottawa DOI | ||
10:05 5mTalk | Automatic Generation of Smoke Test Suites for Kubernetes Tool Demonstrations DOI | ||
10:10 5mTalk | ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC Tool Demonstrations Franz Brausse The University of Manchester, Fedor Shmarov The University of Manchester, Rafael Menezes University of Manchester, Mikhail R. Gadelha Igalia, Konstantin Korovin University of Manchester, Giles Reger University of Manchester, Lucas C. Cordeiro University of Manchester DOI | ||
10:16 5mTalk | ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation Tool Demonstrations Rafael Menezes University of Manchester, Rosiane de Freitas Federal University of Amazonas, Daniel Moura Federal University of Amazonas, Helena Cavalcante Federal University of Amazonas, Lucas C. Cordeiro University of Manchester DOI | ||
10:21 5mTalk | Faster Mutation Analysis with MeMu Tool Demonstrations DOI | ||
10:27 5mTalk | iFixDataloss: A Tool for Detecting and Fixing Data Loss Issues in Android Apps Tool Demonstrations Wunan Guo Fudan University, Zhen Dong Fudan University, China, Liwei Shen Fudan University, Wei Tian Fudan University, Ting Su East China Normal University, Xin Peng Fudan University DOI | ||
10:32 5mTalk | Maestro: A Platform for Benchmarking Automatic Program Repair Tools on Software Vulnerabilities Tool Demonstrations Eduard Costel Pinconschi Instituto Superior Técnico, University of Lisboa & INESC-ID, Quang-Cuong Bui Hamburg University of Technology, Rui Abreu Faculty of Engineering, University of Porto, Portugal, Pedro Adão IST-ULisboa and Instituto de Telecomunicações, Riccardo Scandariato Hamburg University of Technology DOI | ||
10:38 5mTalk | Pytest-Smell: A smell detection tool for Python unit tests Tool Demonstrations Alexandru Bodea Student at Babes Bolay University - Faculty of Mathematics and Computer Science DOI | ||
10:43 5mTalk | QMutPy: A Mutation Testing Tool for Quantum Algorithms & Applications in Qiskit Tool Demonstrations Daniel Fortunato INESC-ID, University of Porto, José Campos Faculty of Engineering of University of Porto & LASIGE, Portugal, Rui Abreu Faculty of Engineering, University of Porto, Portugal DOI | ||
10:49 5mTalk | SpecChecker-ISA: A Data Sharing Analyzer for Interrupt-driven Embedded Software Tool Demonstrations Boxiang Wang Xidian University and Beijing Sunwise Information Technology Ltd, Rui Chen Beijing Institute of Control Engineering, Chao Li Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Tingting Yu Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Dongdong Gao Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Mengfei Yang China Academy of Space Technology, China DOI | ||
10:54 5mTalk | UniRLTest: Universal Platform-Independent Testing with Reinforcement Learning via Image Understanding Tool Demonstrations Ziqian Zhang Nanjing University, Yulei Liu Nanjing University, Shengcheng Yu Nanjing University, Xin Li Nanjing University, Yexiao Yun Nanjing University, Chunrong Fang Nanjing University, Zhenyu Chen Nanjing University DOI | ||