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 :
Journal articles
Complete list of metadatas

Cited literature [35 references]  Display  Hide  Download
Contributor : Léna Le Roy <>
Submitted on : Thursday, January 10, 2019 - 9:45:34 AM
Last modification on : Friday, July 26, 2019 - 4:26:20 PM
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. Lecture Notes in Computer Science, Springer, 2016, 9633, pp.179-196. ⟨10.1007/978-3-662-49665-7_11⟩. ⟨cea-01808894⟩



Record views


Files downloads