Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis

Omar Chebaro 1 Nikolai Kosmatov 1 Alain Giorgetti 2, 3 Jacques Julliand 2
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Recent research proposed efficient methods for software verification combining static and dynamic analysis, where static analysis reports possible runtime errors (some of which may be false alarms) and test generation confirms or rejects them. However, test generation may time out on real-sized programs before confirming some alarms as real bugs or rejecting some others as unreachable. To overcome this problem, we propose to reduce the source code by program slicing before test generation. This paper presents new optimized and adaptive usages of program slicing, provides underlying theoretical results and the algorithm these usages rely on. The method is implemented in a tool prototype called sante (Static ANalysis and TEsting). Our experiments show that our method with program slicing outperforms previous combinations of static and dynamic analysis. Moreover, simplifying the program makes it easier to analyze detected errors and remaining alarms.
Type de document :
Communication dans un congrès
SAC 2012, 27-th ACM Symposium On Applied Computing, Mar 2012, Trento, Italy. ACM, pp.1284-1291, 2012, Proceedings of the 27th Annual ACM Symposium on Applied Computing. 〈10.1145/2245276.2231980〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00746814
Contributeur : Alain Giorgetti <>
Soumis le : lundi 29 octobre 2012 - 17:17:01
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

Citation

Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand. Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis. SAC 2012, 27-th ACM Symposium On Applied Computing, Mar 2012, Trento, Italy. ACM, pp.1284-1291, 2012, Proceedings of the 27th Annual ACM Symposium on Applied Computing. 〈10.1145/2245276.2231980〉. 〈hal-00746814〉

Partager

Métriques

Consultations de la notice

311