Cut branches before looking for bugs: certifiably sound verification on relaxed slices

Program slicing can be used to reduce a given initial program to a smaller one (a slice ) that preserves the behavior of the initial program with respect to a chosen criterion. Verification and validation (V&V) of software can become easier on slices, but require particular care in the presence of errors or non-termination in order to avoid unsound results or a poor level of code reduction in slices with respect to the initial program. This article proposes a theoretical foundation for conducting V&V activities on a slice instead of the initial program. We introduce the notion of relaxed slicing that is still capable of producing small slices, even in the presence of errors or non-termination, and establish an appropriate soundness property. It allows us to give a precise interpretation of verification results (absence or presence of errors) obtained for a slice in terms of the initial program. The implementation of these results in the Coq proof assistant is presented and some of its difficult points are discussed.