How Test Generation Helps Software Specification and Deductive Verification in Frama-C

Guillaume Petiot 1, 2 Nikolai Kosmatov 1 Alain Giorgetti 3, 2 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 : This paper describes an incremental methodology of deductive verification assisted by test generation and illustrates its benefits by a set of frequent verification scenarios. We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform FramaC. This new plugin treats a complete formal specification of a C program during test generation and provides the validation engineer with a helpful feedback at all stages of the specification and verification tasks.
Type de document :
Communication dans un congrès
Martina Seidl, Nikolai Tillmann. Tests and Proofs, Jul 2014, York, United Kingdom. Springer, 8570, pp.204 - 211, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-09099-3_16〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01108553
Contributeur : Alain Giorgetti <>
Soumis le : vendredi 23 janvier 2015 - 08:37:54
Dernière modification le : lundi 24 septembre 2018 - 11:34:02
Document(s) archivé(s) le : vendredi 24 avril 2015 - 10:11:18

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand. How Test Generation Helps Software Specification and Deductive Verification in Frama-C. Martina Seidl, Nikolai Tillmann. Tests and Proofs, Jul 2014, York, United Kingdom. Springer, 8570, pp.204 - 211, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-09099-3_16〉. 〈hal-01108553〉

Partager

Métriques

Consultations de la notice

491

Téléchargements de fichiers

188