Available slicing methods Syntactic: Use syntactic slicing IAA - Impact Analysis for Assignments: does an information flow check from each assignment to the criterion, for each assignment. If there is no information flow the assignment is removed. SLE - Single Line Elimination: try to removes a lines and verifies if the slice candidate is still a valid slice. If it is not, then the line is added again. Repeated until no further lines can be removed. CGS - Counterexample Guided Slicing: Union of dynamic slices generated from counter examples until the slice is valid. Note, that this method is not yet able to deal with arrays and heaps.