Andrew Santosa
University of Sydney

Path-Sensitive Backward Slicing

Backward slicers are typically path-insensitive (i.e., they ignore the
evaluation of predicates in guards), or they are only partial sometimes
producing too big slices. Though the value of path-sensitivity is always
desirable, the major challenge is that there are, in general, an exponential
number of predicate combinations to be considered. We present a path-sensitive
backward slicer and demonstrate its practicality with real C programs. The
core is a symbolic execution-based algorithm that employs an approximation of
weakest precondition using Craig's interpolation, to exclude spurious
dependencies lying on infeasible paths while pruning paths that cannot improve
the accuracy of the dependencies already computed by other paths.