Cut branches before looking for bugs: certifiably sound verification on relaxed slices - Archive ouverte HAL Access content directly
Journal Articles Formal Aspects of Computing Year : 2018

Cut branches before looking for bugs: certifiably 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) 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.
Not file

Dates and versions

cea-01801601 , version 1 (28-05-2018)

Identifiers

Cite

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⟩
61 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More