On-the-fly model checking under fairness that exploits symmetry

Abstract

An on-the-fly algorithm, for model checking under fairness, is presented. The algorithm utilizes symmetry in the program to reduce the state space, and employs new novel techniques that make the on-the-fly model checking feasible. The algorithm uses state symmetry and eliminates paralle edges in the reachability graph. Experimental results, demonstrating dramatic reductions in both the running time and memory usage, are presented.