In short: What is the basic difference that allows model checking for hardware to be "easily" solvable, but makes it undecidable for software?
I guess it has to boil down to the difference between hardware being finite automata and software having the expressiveness of a Turing machine, which would basically mean that its the infinite amount of (randomly accessible, vs. that of a push-down automaton) memory that the Turing machine has available -- is this correct?
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).
