Model checking method for program using program slicing

摘要

It is important to verify behavior of programs and guarantee qualities. It is possible to define programs on transition systems and check the model, however large and complex models don't suit for model checking. In this paper we propose model checking method for program using program slicing. Automatic verification is possible, because we extract from C program relating arbitrary instruction and construct finite state transition system. Finally, we show our methods by verification using SMV.