Exploiting Symmetry When Model-Checking Software

Abstract

We study how to exploit symmetry induced by identical processes or data structures when systematically exploring the state spaces of concurrent software applications such as implementations of communication protocols. Existing model-checking symmetry reduction methods are based on equivalence classes of states, and assume that every system state can easily be encoded by a unique string of bits. When dealing with processes described by software programs written in full-fledged programming languages such as C, C++ or Java, this assumption is not valid anymore. Indeed, the state of each process is determined by the values of all the memory locations that can be accessed by the process and influence its behavior (including activation records associated to procedure calls). This amount of information is typically far too large and complex to be efficiently computed at each step of a state-space exploration We develop in this paper a simple theory based on equivalence classes of sequences of transitions for representing symmetries in a system. We then present a state-space exploration algorithm for exploiting symmetries on transitions which does not rely on explicit encodings of system states. This algorithm can be used to dynamically prune the state spaces of implementations of concurrent reactive software systems in a reliable way.