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 metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01108553
Contributor : Alain Giorgetti <>
Submitted on : Friday, January 23, 2015 - 8:37:54 AM
Last modification on : Thursday, February 7, 2019 - 4:01:30 PM
Long-term archiving on : Friday, April 24, 2015 - 10:11:18 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

577

Files downloads

263