Skip to Main content Skip to Navigation
Conference papers

Cut branches before looking for bugs: Sound verification on relaxed slices

Abstract : Program slicing can be used to reduce a given initial program to a smaller one (a slice) which 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 presence of errors or non-termination in order to avoid unsound results or a poor level of reduction in slices. 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 remains efficient even in 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. Our results have been proved in Coq.
Document type :
Conference papers
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Léna Le Roy Connect in order to contact the contributor
Submitted on : Thursday, January 10, 2019 - 9:45:34 AM
Last modification on : Thursday, February 17, 2022 - 10:08:06 AM
Long-term archiving on: : Thursday, April 11, 2019 - 1:53:33 PM


Files produced by the author(s)



J.-C. Léchenet, N. Kosmatov, P. Le Gall. Cut branches before looking for bugs: Sound verification on relaxed slices. International Conference on Fundamental Approaches to Software Engineering, Apr 2016, Eindhoven, Netherlands. pp.179-196, ⟨10.1007/978-3-662-49665-7_11⟩. ⟨cea-01808894⟩



Record views


Files downloads