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

Abstract : 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. © 2017, British Computer Society.
Document type :
Journal articles
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01801601
Contributor : Léna Le Roy <>
Submitted on : Monday, May 28, 2018 - 3:32:15 PM
Last modification on : Thursday, February 7, 2019 - 4:02:48 PM

Identifiers

Citation

J.-C. Léchenet, N. Kosmatov, P. Le Gall. Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects of Computing, 2018, 30 (1), pp.107-131. ⟨10.1007/s00165-017-0439-x⟩. ⟨cea-01801601⟩

Share

Metrics

Record views

82