Why might model checking fail?
Software is often specified with infinite state descriptions
- We don’t address those specifications
- Jackson, Damon, Jha; Wing, Vaziri-Farahani; etc.
Software specifications may be structured differently from hardware specifications
- Hierarchy
- Representations and algorithms for model checking may not scale