Relaxed Slicing

This site presents a formalization in the Coq proof assistant of program slicing and its correctness for a simple language with possible non-termination and runtime errors, and its application to verification.

This work is also detailed in the associated publications.

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.

Theorems for Relaxed Slicing

Soundness Property

Relaxed slicing satifies a new soundness property, which states that the projection of the trajectory of the initial program is a prefix of the projection of the trajectory of the slice. For a given input, if the program terminates without provoking an error, then the projections are equal.

Results for Verification

We can deduce from this theorem two results for verification.

If there are no runtime errors in the slice, then there are none in the original program, in the statements preserved in the slice.

If there is a runtime error in the slice, then either the same error occurs in the original program, or another error or an infinite loop caused by a statement not preserved in the slice masks it.

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.