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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Exploration algorithms for explicit-state transition systems are a coreback-end technology in program verification. They can be applied to programs bygenerating the transition system on the fly, avoiding an expensive up-fronttranslation. An on-the-fly strategy requires significant modifications to theimplementation, into a form that stores states directly as valuations ofprogram variables. Performed manually on a per-algorithm basis, suchmodifications are laborious and error-prone.  In this paper we present the IJIT Application Programming Interface (API),which allows users to automatically transform a given transition systemexploration algorithm to one that operates on Boolean programs. The APIconverts system states temporarily to program states just in time for expansionvia image computations, forward or backward. Using our API, we haveeffortlessly extended various non-trivial (e.g. infinite-state) model checkingalgorithms to operate on multi-threaded Boolean programs. We demonstrate theease of use of the API, and present a case study on the impact of thejust-in-time translation on these algorithms.

IJIT: An API for Boolean Program Analysis with Just-in-Time Translation (Extended Technical Report)