Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Alain Giorgetti Connect in order to contact the contributor
Submitted on : Friday, January 23, 2015 - 8:37:54 AM
Last modification on : Saturday, June 25, 2022 - 9:09:20 PM
Long-term archiving on: : Friday, April 24, 2015 - 10:11:18 AM


Files produced by the author(s)



Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand. How Test Generation Helps Software Specification and Deductive Verification in Frama-C. Tests and Proofs, Jul 2014, York, United Kingdom. pp.204 - 211, ⟨10.1007/978-3-319-09099-3_16⟩. ⟨hal-01108553⟩



Record views


Files downloads