A New Approach to Stateless Model Checking of LTL Properties

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.