Why might it fail?
Software is often specified with infinite
state descriptions
Software specifications may be structured
differently from hardware specifications
Hierarchy
Representations and algorithms for model
checking may not scale