Check out the new USENIX Web site. next up previous
Next: CMC Infrastructure Up: CMC: A Pragmatic Approach Previous: Model Checking Overview

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.


Madanlal Musuvathi 2002-10-08