This paper revies finite and infinite-state model checking form two pragmatic perspectives: the application to the static analysis of imperative programs or data flow analysis, and the implementational aspect. Data flow analysis provides an interesting area of application for model checking, which is particularly challenging in the interprocedural case, since infinite state spaces need to be considered. Moreover, as it is a typical case of a structurally unrestricted problem, one should use global iterative methods for solution. This can be exploited for a uniform and efficient treatment based on a fixpoint analysis machine that covers all kinds of logics and model structures important for the considered application.
cetindag@fmi.uni-passau.de
>
Ulrike Peiker, Martin Griebl