English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In this work, we describe and evaluate the first model checker for verifyingKotlin programs through the Jimple intermediate representation. The verifier,named ESBMC-Jimple, is built on top of the Efficient SMT-based Context-BoundedModel Checker (ESBMC). It uses the Soot framework to obtain the Jimple IR,representing a simplified version of the Kotlin source code, containing amaximum of three operands per instruction. ESBMC-Jimple processes Kotlin sourcecode together with a model of the standard Kotlin libraries and checks a set ofsafety properties. Experimental results show that ESBMC-Jimple can correctlyverify a set of Kotlin benchmarks from the literature and that it iscompetitive with state-of-the-art Java bytecode verifiers. A demonstration isavailable at https://youtu.be/J6WhNfXvJNc.

ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation