My introduction to predicate abstraction (not the first work to make use of it), another interesting technique. Basic idea is: you have some complicated state in your program that is causing your model checker to blow up (i.e. consider too many states), replace it with a predicate over that state that captures whatever it is that your program cares about. Maybe you have two timer variables that could in theory each take on any 64-bit value, but all you care about is whether one is greater than the other. You can reduce 2^128 possible states to 2. Big win. In this case, they used it to apply model checking directly to the source code of a real-time OS kernel.