Designing executable abstractions

Abstract

It is well-known that in general the problem of deciding whether a program halts (or can dead-lock) 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.