CMC: A Pragmatic Approach to Model Checking Real Code

Many system errors do not emerge unless some intricate sequence of events occurs. In practice, this means that most systems have errors that only trigger after days or weeks of execution. Model checking [4] is an effective way to find such subtle errors. It takes a simplified description of the code and exhaustively tests it on all inputs, using techniques to explore vast state spaces efficiently. Unfortunately, while model checking systems code would be wonderful, it is almost never done in practice: building models is just too hard. It can take significantly more time to write a model than it did to write the rthermore, by checking an abstraction of the code rather than the code itself, it is easy to miss errors. The paper's first contribution is a new model checker, CMC, which checks C and C++ implementations , eliminating the need for a separate abstract description of the system behavior. This has two major advantages: it reduces the effort to use model checking, and it redu...

• Type: Conference
• Year: 2002
• Where: OSDI
• Authors: Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, David L. Dill
• Keywords: Missed Errors, Model Checking, Model Checking Systems, Operating System, OSDI 2002