The state explosion problem is becoming less of an issue in software nowadays because of the massive improvement in SAT/SMT solvers. The topic of this post is not about model checking, but I believe still interesting.
One big improvement when it came to verification came from symbolic execution [1], in which the verifier looks for assertion violations by representing variables as a set of constraints. At each assertion, the constraints are checked to see if they can be negatively satisfied, giving a counterexample for the error. We run the program in a special interpreter (or using some interesting metaprogramming and a compiler frontend etc) and at each conditional statement a new constraint is added, leading to a tree. By cleverly picking branches etc we hopefully drastically reduce the search space.
This reduced the state explosion problem in many cases, but obviously there's now an explosion on the control flow. A more recent improvement has been to unwind loops a bound number of times, encoding the whole program as a logical statement that is only satisfied by input that will trigger an assertion error. The hypothesis is that the structure of such formulas is well simplified by SAT solvers, and this has been borne out empirically from what I know. We can further improve by natively executing that code which is not constrained, which is a further boon - in principle we could instrument a program to simply return the formula that (if satisfied) produces counterexamples.
This sort of approach is very useful in practice because it's very understandable to software engineers - in the ideal case where a large company produces a product based on it, one might reasonably expect to be able to pass the software their source code and be presented with a series of counterexamples. It's all very interesting.
(I'm not an expert on this, take what I say with a pinch of salt).
> A more recent improvement has been to unwind loops a bound number of times, encoding the whole program as a logical statement that is only satisfied by input that will trigger an assertion error.
The technical term for this is bounded model checking (BMC).
One big improvement when it came to verification came from symbolic execution [1], in which the verifier looks for assertion violations by representing variables as a set of constraints. At each assertion, the constraints are checked to see if they can be negatively satisfied, giving a counterexample for the error. We run the program in a special interpreter (or using some interesting metaprogramming and a compiler frontend etc) and at each conditional statement a new constraint is added, leading to a tree. By cleverly picking branches etc we hopefully drastically reduce the search space.
This reduced the state explosion problem in many cases, but obviously there's now an explosion on the control flow. A more recent improvement has been to unwind loops a bound number of times, encoding the whole program as a logical statement that is only satisfied by input that will trigger an assertion error. The hypothesis is that the structure of such formulas is well simplified by SAT solvers, and this has been borne out empirically from what I know. We can further improve by natively executing that code which is not constrained, which is a further boon - in principle we could instrument a program to simply return the formula that (if satisfied) produces counterexamples.
This sort of approach is very useful in practice because it's very understandable to software engineers - in the ideal case where a large company produces a product based on it, one might reasonably expect to be able to pass the software their source code and be presented with a series of counterexamples. It's all very interesting.
(I'm not an expert on this, take what I say with a pinch of salt).
[1] https://klee.github.io/klee/