TITLE: Slicing Software for Model Construction
AUTHORS: John Hatcliff, Matthew B. Dwyer, Hongjun Zheng
Applying finite-state verification techniques (e.g., model checking) to
software requires that program source code be translated to a
finite-state transition system that safely models program behavior.
Automatically checking such a transition system for a correctness
property is typically very costly, thus it is necessary to reduce the
size of the transition system as much as possible. In fact, it is
often the case that much of a program's source code is irrelevant for
verifying a given correctness property.
In this paper, we apply program slicing techniques to remove
automatically such irrelevant code and thus reduce the size of the
corresponding transition system models. We give a simple extension of
the classical slicing definition, and prove its safety with respect to
model checking of linear temporal logic (LTL) formulae. We discuss
how this slicing strategy fits into a general methodology for deriving
effective software models using abstraction-based program
specialization.