Model Checking: hardware vs software
The statespace explosion problem.

More specifically, software often uses unbounded loops, pointers into complex data structures on the heap, and dynamic allocation.  Each of these can cause rapid statespace explosion: the number of states increases rapidly, or becomes infinite.  Model checking has difficulty with that.  These constructs tend to be more common in software than in hardware, explaining why model checking tends to be more effective on hardware than on software (as a general rule, though there are of course exceptions).