A New Approach to Stateless Model Checking of LTL Properties

TL;DR

This paper introduces a novel actor-based encoding for LTL semantics on finite paths, enabling parallel stateless model checking of concurrent programs without storing states or traces.

Contribution

It presents a new parallel approach to LTL verification that integrates with stateless model checking, addressing limitations of existing tools.

Findings

Supports LTL properties in stateless model checking

Enables truly parallel verification without state storage

Applicable to large, complex concurrent programs

Abstract

Verification of large and complicated concurrent programs is an important issue in the software world. Stateless model checking is an appropriate method for systematically and automatically testing of large programs, which has proved its power in verifying code of large programs. Another well-known method in this area is runtime verification. Both stateless model checking and runtime verification are similar in some ways. One common approach in runtime verification is to construct runtime monitors for properties expressed in linear temporal logic. Currently, there are some semantics to check linear temporal logic formulae on finite paths proposed in the field of runtime verification, which can also be applied to stateless model checking. However, existing stateless model checkers do not support LTL formulae. In some settings, it is more advantageous to make use of stateless model checking instead of runtime verification. This paper proposes a novel encoding of one of the recent LTL semantics on finite paths into an actor-based system. We take a truly parallel approach without saving any program states or traces, which not only addresses important problems in runtime verification, but can also be applied to stateless model checking.