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?

  • 3
    $\begingroup$ You answered your own question. $\endgroup$ – Dave Clarke Oct 25 '14 at 12:14

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).

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.