Bandera uses both program slicing and data abstraction
(abstract interpretation) to customize models. The Bandera program
slicer takes as input all the observables mentioned in the input
property 
. These observables may reference particular program
variables and control points. The semantics of these program features
must be preserved for correctly checking , but all other
program components that don't influence the semantics of the
observable features can be eliminated in the generated model. The
program slicer builds a program dependence graph representing
several different forms of dependence, and it will generate
an executable residual program (the program slice) where
components that do not influence the execution of the
observables in have been removed. The sliced
program is created at the Jimple level, but it can also be
decompiled to Java source using JJJC. For more details,
we refer the reader to formalizations
of the Bandera slicer's approach to property-driven
slicing [10], and the notions of program dependence
required for slicing the concurrent features of Java [9].