Cut branches before looking for bugs: Sound verification on relaxed slices - Archive ouverte HAL Access content directly
Conference Papers Year : 2016

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

(1, 2) , (1) , (2)
1
2

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.
Fichier principal
Vignette du fichier
Lechenet2016.pdf (364.74 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

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

Identifiers

Cite

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⟩
55 View
140 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More