Cut branches before looking for bugs: Sound verification on relaxed slices
In: International Conference on Fundamental Approaches to Software Engineering International Conference on Fundamental Approaches to Software Engineering, Apr 2016, Eindhoven, Netherlands. pp.179-196, ⟨10.1007/978-3-662-49665-7_11⟩ Fundamental Approaches to Software Engineering ISBN: 9783662496640 FASE Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2016, 9633, pp.179-196. 〈10.1007/978-3-662-49665-7_11〉; (2016-04-02)
Online
unknown
Zugriff:
Conference of 19th International Conference on Fundamental Approaches to Software Engineering, FASE 2016 Held as Part of European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference Date: 2 April 2016 Through 8 April 2016; Conference Code:172399; International audience; 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.
| Titel: |
Cut branches before looking for bugs: Sound verification on relaxed slices
|
|---|---|
| Autor/in / Beteiligte Person: | Pascale Le Gall ; Léchenet, Jean-Christophe ; Kosmatov, Nikolai ; Département Ingénierie Logiciels et Systèmes (DILS) ; Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)) ; Direction de Recherche Technologique (CEA) (DRT (CEA)) ; Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)) ; Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay ; Mathématiques et Informatique pour la Complexité et les Systèmes (MICS) ; CentraleSupélec ; European Project: 621353,EC:FP7:SP1-JTI,ARTEMIS-2013-1,DEWI(2014) ; Laboratoire d'Intégration des Systèmes et des Technologies (LIST) ; Département Ingénierie Logiciels et Systèmes ( DILS ) ; Laboratoire d'Intégration des Systèmes et des Technologies ( LIST ) ; Commissariat à l'énergie atomique et aux énergies alternatives ( CEA ) -Université Paris-Saclay-Commissariat à l'énergie atomique et aux énergies alternatives ( CEA ) -Université Paris-Saclay ; Mathématiques et Informatique pour la Complexité et les Systèmes ( MICS ) ; European Project : 621353,EC:FP7:SP1-JTI,ARTEMIS-2013-1,DEWI ( 2014 ) |
| Link: | |
| Quelle: | International Conference on Fundamental Approaches to Software Engineering International Conference on Fundamental Approaches to Software Engineering, Apr 2016, Eindhoven, Netherlands. pp.179-196, ⟨10.1007/978-3-662-49665-7_11⟩ Fundamental Approaches to Software Engineering ISBN: 9783662496640 FASE Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2016, 9633, pp.179-196. 〈10.1007/978-3-662-49665-7_11〉; (2016-04-02) |
| Veröffentlichung: | HAL CCSD, 2016 |
| Medientyp: | unknown |
| ISBN: | 978-3-662-49664-0 (print) |
| Schlagwort: |
|
| Sonstiges: |
|