Design of CMC

CMC is a model checker that generates the state space of a given
system by directly executing its C or C++ implementation. This
section describes the design of CMC, beginning with a description of
the tool's infrastructure. The steps required to set up a system for
checking are described and illustrated with an example. The
actual model checking algorithm then follows. Finally, some
techniques to cope with the *state explosion problem* are
discussed.

- CMC Infrastructure
- Creating a CMC Model from the Implementation
- CMC Model Checking Algorithm

- Handling State Space Explosion

Madanlal Musuvathi 2002-10-08