The article presents the SMC system. SMC can be used 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 by exploiting symmetries of the input concurrent program, usually present in the form of identical processes, in two different ways. Firstly, 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 . Secondly, it reduces the number of edges explored from each state, in0 the reduced state graph, by exploiting the symmetry of a single state; this is 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” high-speed serial bus protocol. SMC found deadlocks in the protocol. SMC was also to check certain liveness properties. A report on the case study is included in the article.

Abstract. The paper proposes an induction based approach, that employs automata as inductive invariants, for verifying safety and liveness properties of linear networks of arbitrary size. The proposed method has been shown to be complete for verifying safety properties. Automated methods that check for correcteness of such families of networks are proposed. These methods are based on generating an invariant automaton from the correctness property which is also specified by an automaton. These methods have been implemented and successfully tested on some examples.