Static Backward Slicing
Introduced in 1981 by Weiser, static backward slicing is a method which, given an initial program,
computes a simpler program, the slice,
with respect to a slicing criterion, typically a statement.
Informally speaking, the classic soundness property states that in case of normal termination,
the program and its slice have the same behavior.
Formally, in terms of trajectory-based semantics,
if the execution of the original program terminates without error on a given input state,
then the execution of the slice terminates too, and the projections of the trajectories
of both programs are equal.
Relaxed Slicing
The classic soundness property presented above does not say anything
about programs containing errors or non-termination. And actually, it does not hold in this
more general case.
Adding more dependencies to keep the classic property at the cost of getting bigger slices is the easiest solution.
We prefer keeping basically the same dependencies, and weakening the soundness property. That is what we call relaxed slicing.
Coq Formalization
Relaxed slicing has been formalized in the Coq proof assistant for a simple imperative language. The Coq development, available for educational, research or evaluation purposes only, can be found here. You can also browse the documentation online here.