SMC: A Symmetry Based Model Checker for Verification of Safety and Liveness Properties

The paper presents the SMC system for checking safety and liveness properties of concurrent programs under different fairness assumptions. It is based on explicit state enumeration; it combats the state explosion problem by utilizing symmetries of the input concurrent program usually present in the form of identical processes. It reduces the number of explored states by identifying those states that are equivalent under the symmetries of the system; this is called process symmetry. It reduces the number of edges explored from each state by exploiting the symmetry of a single state, called state symmetry. SMC works in an on-the-fly manner, it constructs the reduced state graph as and when it is needed. This method facilitates early termination, speeds up model-checking and reduces memory requirements. We employed SMC to check the correctness of, among other standard examples, the Link Layer part of the IEEE Standard 1394 "Firewire" highspeed serial bus protocol. SMC found some deadlock..