Symmetry reductions for model checking of concurrent dynamic software

International audienceSymmetry reduction techniques exploit symmetries that occur during the execution of a system in order to minimize its state space for efficient verification of temporal logic properties. This paper presents a framework for concisely defining and evaluating symmetry reductions currently used in software model checking, involving heap objects and processes. An on-the-fly state space exploration algorithm combining both techniques will also be presented. Second, the relation between symmetry and partial-order reductions is investigated, showing how one’s strengths can be used to compensate for the other’s weaknesses. The symmetry reductions presented here were implemented in the dSPIN model-checking tool. We also performed a number of experiments that show significant progress in reducing the cost of finite-state software verification