Designing executable abstractions
Gerard J. Holzmann · 1998
It is well-known that in general the problem of deciding whether a program halts (or can deadlock) is undecidable.Model checkers, therefore, cannot be applied to arbitrary programs, but work with well-defined abstractions of programs.The feasibility of a verification often depends on the type of abstraction that is made.Abstraction is indeed the most powerful tool that the user of a model checking tool can apply, yet it is often perceived as a temporary inconvenience.1.1