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 [7 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01808894
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

File

Lechenet2016.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

110

Files downloads

81