Pp. 75-88 of the Proceedings

Next: Abstract

CMC: A Pragmatic Approach to Model Checking Real Code

Madanlal Musuvathi¹, David Y.W. Park², Andy Chou,
Dawson R. Engler, David L. Dill

{madan, parkit, acc, engler, dill}@cs.stanford.edu
Computer Systems Laboratory
Stanford University
Stanford, CA 94305, U.S.A

• • Abstract
  
  
• Introduction
• Model Checking Overview
• Design of CMC
  • CMC Infrastructure
  • Creating a CMC Model from the Implementation
  • CMC Model Checking Algorithm
    • Generating the Initial State
    • Generating Successor States
    • Checking Correctness Properties
  • Handling State Space Explosion
  
  
• Description of the AODV Protocol
• The AODV model
• Results
• Related Work
• Conclusion and Future Work
• Acknowledgments
• Bibliography
• About this document ...