General Terms
Categories and Subject Descriptors
1. INTRODUCTION
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
SoftMC ’03, July 18–19, 2002, Boulder, CO, USA.
Copyright 2003 ACM 1-58113-479=7/02/0011 ... 5.00.
1.1 The model checking approach
1.2 The static analysis approach
2. CASE STUDY: FLASH
2.1 FLASH overview
2.2 Checking FLASH with static analysis
2.3 Model checking FLASH
3. LESSONS FROM FLASH
3.1 Observed model checking advantages
4. CASE STUDY: AODV
4.1 CMC Overview
4.2 AODV Overview
4.3 Model Checking AODV with CMC
4.4 Comparison with Static Analysis
5. CASE STUDY: TCP
5.1 Difficulties in Environment Modeling
5.1.1 Failed Approach: The TCP Library Model
5.1.2 Hard Learned Lessons
5.2 The Linux TCP Model
5.3 Measuring the Search Effectiveness
5.4 Iterative Environment Refinement
5.5 TCP Model Checking Results
5.6 Lessons from Model Checking TCP
6. GENERAL LESSONS
6.1 Myth: model checking = no false positives
6.2 Ease-of-inspection really matters
6.3 Myth: more analysis is always better
6.4 Myth: all bugs matter
7. RELATED WORK
8. CONCLUSION
9. ACKNOWLEDGMENTS
10. REFERENCES
APPENDIX
A. CHECKER EXAMPLE
