Cut branches before looking for bugs: Sound verification on relaxed slices - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

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

Résumé

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.
Fichier principal
Vignette du fichier
Lechenet2016.pdf (364.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

cea-01808894 , version 1 (10-01-2019)

Identifiants

Citer

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⟩
61 Consultations
165 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More