DSCMC: Distributed Stateless Code Model Checker

TL;DR

DSCMC is a distributed, actor-based stateless code model checker that verifies multi-language code for deadlocks, livelocks, data races, LTL properties, and information flow security, leveraging Erlang's concurrency.

Contribution

It introduces a distributed, actor-based architecture for stateless code model checking capable of verifying complex properties across multiple programming languages.

Findings

Detects deadlocks, livelocks, and data races automatically

Verifies LTL properties and information flow security

Utilizes Erlang's concurrency for efficient parallel checking

Abstract

Stateless code model checking is an effective verification technique, which is more applicable than stateful model checking to the software world. Existing stateless model checkers support the verification of neither LTL formulae nor the information flow security properties. This paper proposes a distributed stateless code model checker (DSCMC) designed based on the Actor model, and has the capability of verifying code written in different programming languages. This tool is implemented using Erlang, which is an actor-based programming language. DSCMC is able to detect deadlocks, livelocks, and data races automatically. In addition, the tool can verify information flow security and the properties specified in LTL. Thanks to its actor-based architecture, DSCMC provides a wide range of capabilities. The parallel architecture of the tool exploiting the rich concurrency model of Erlang is suited to the time-intensive process of stateless code model checking.