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.
Type de document :
Article dans une revue
Formal Aspects of Computing, 2018, 30 (1), pp.107-131. 〈10.1007/s00165-017-0439-x〉
Liste complète des métadonnées

https://hal-cea.archives-ouvertes.fr/cea-01801601
Contributeur : Léna Le Roy <>
Soumis le : lundi 28 mai 2018 - 15:32:15
Dernière modification le : lundi 24 septembre 2018 - 11:34:03

Identifiants

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〉

Partager

Métriques

Consultations de la notice

48