Check out the new USENIX Web site. next up previous
Next: Generating the Initial State Up: Design of CMC Previous: Creating a CMC Model

CMC Model Checking Algorithm

Given a model of the system built as described above, CMC explores the state space of the system by executing various traces of interleaving transitions. The pseudocode for the algorithm is shown in Figure 3. The algorithm maintains two data structures: a hash table of states seen during the search, and a queue of states seen but whose successors are yet to be generated. The hash table guarantees that the algorithm explores the subgraph rooted at a state at most once.


Madanlal Musuvathi 2002-10-08