Model checking for programming languages using VeriSoft

TLDR

Model checking is an effective method for analyzing concurrent reactive systems, but current techniques are limited to verifying properties of abstract models rather than actual implementations. The paper aims to extend model checking to directly verify implementations of concurrent systems written in languages such as C or C++. The authors introduce a new search technique implemented in VeriSoft to systematically explore state spaces of concurrent processes executing arbitrary C code. VeriSoft discovered an error in a 2500‑line C program that controls robots in an unpredictable environment.

Abstract

Verification by state-space exploration, also often referred to as "model checking", is an effective method for analyzing the correctness of concurrent reactive systems (e.g., communication protocols). Unfortunately, existing model-checking techniques are restricted to the verification of properties of models, i.e., abstractions, of concurrent systems.In this paper, we discuss how model checking can be extended to deal directly with "actual" descriptions of concurrent systems, e.g., implementations of communication protocols written in programming languages such as C or C++. We then introduce a new search technique that is suitable for exploring the state spaces of such systems. This algorithm has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C code. As an example of application, we describe how VeriSoft successfully discovered an error in a 2500-line C program controlling robots operating in an unpredictable environment.