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

TL;DR

The paper introduces the IJIT API, enabling automatic on-the-fly translation of transition systems to Boolean programs, simplifying the extension of model checking algorithms to handle complex, multi-threaded programs efficiently.

Contribution

The IJIT API automates the transformation of exploration algorithms to operate on Boolean programs, reducing manual effort and errors in on-the-fly transition system analysis.

Findings

API simplifies extension of algorithms to Boolean programs

Enables handling of multi-threaded infinite-state systems

Demonstrates effectiveness through case studies

Abstract

Exploration algorithms for explicit-state transition systems are a core back-end technology in program verification. They can be applied to programs by generating the transition system on the fly, avoiding an expensive up-front translation. An on-the-fly strategy requires significant modifications to the implementation, into a form that stores states directly as valuations of program variables. Performed manually on a per-algorithm basis, such modifications 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 system exploration algorithm to one that operates on Boolean programs. The API converts system states temporarily to program states just in time for expansion via image computations, forward or backward. Using our API, we have effortlessly extended various non-trivial (e.g. infinite-state) model checking algorithms to operate on multi-threaded Boolean programs. We demonstrate the ease of use of the API, and present a case study on the impact of the just-in-time translation on these algorithms.