CMC: A Pragmatic Approach to Model Checking Real Code

From GradTurkey

[edit] Summary

The authors present a model checker that works directly on C and C++ code, motivated by the false positives and false negatives that can occur when code does not match a separately developed model, and also that models can take even longer to write than the original code. The checker can deal reasonably well with the state space of event-driven network protocol implementations, which they analyze and find numerous bugs. The exploration always runs out of space due to state-space explosion, but finds significant bugs before then by recognizing equivalent heap structures, reducing the number of concurrent processes, and additional heuristics. The longest it took to find any of the bugs in their examples was 40 minutes.

[edit] BibTeX Entry

@InProceedings{MusuvathiParkChouEnglerDill2002,
  crossref  = {osdi2002},
  author    = {Madanlal Musuvathi and David Y. W. Park and Andy Chou and Dawson R. Engler and David L. Dill},
  title     = {CMC: A Pragmatic Approach to Model Checking Real Code},
}