This paper was part of my introduction to model checking. It introduces an idea that has gotten a lot of mileage in the program analysis and model checking community. To wit: start with a rough (but soundly over-approximating) abstraction, if said abstraction demonstrates a violation figure out whether the violation is real (you’re done) or spurious, in the latter case use the spurious example to refine your abstraction as little as possible. Repeat until your abstraction is sufficiently refined to find a real violation or no violations.