Skip to Main content Skip to Navigation
Conference papers

A Late Treatment of C Precondition in Dynamic Symbolic Execution

Mickaël Delahaye 1 Nikolai Kosmatov 2 
1 VASCO - Validation de Systèmes, Composants et Objets logiciels
LIG - Laboratoire d'Informatique de Grenoble
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : Relevance of automatically generated test cases depends on an appropriate definition of a test context, or precondition. This paper presents a novel method for handling a precondition in dynamic symbolic execution (DSE) testing tools. This method allows Path Crawler, a DSE tool for C~programs, to accept a precondition defined as a C function. It provides a simple way to express a precondition even for developers who are not familiar with specification formalisms. It has also proven useful when combining static and dynamic analysis.
Document type :
Conference papers
Complete list of metadata
Contributor : Mickaël Delahaye Connect in order to contact the contributor
Submitted on : Friday, August 23, 2013 - 7:36:47 PM
Last modification on : Wednesday, July 6, 2022 - 4:17:28 AM




Mickaël Delahaye, Nikolai Kosmatov. A Late Treatment of C Precondition in Dynamic Symbolic Execution. CSTVA 2013 - 5th International Workshop on Constraints in Software Testing, Verification, and Analysis, Aug 2013, Luxembourg, Luxembourg. pp.230-231, ⟨10.1109/ICSTW.2013.34⟩. ⟨hal-00853725⟩



Record views