Skip to Main content Skip to Navigation
Conference papers

A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools

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 : This paper presents a novel technique for handling a precondition in dynamic symbolic execution (DSE) testing tools. It delays precondition constraints until the end of the program path evaluation. This method allows PathCrawler, a DSE tool for C programs, to accept a precondition defined as a C function. It provides a convenient way to express a precondition even for developers who are not familiar with specification formalisms. Our initial experiments show that it is more efficient than early precondition treatment, and has a limited overhead compared to a native treatment of a precondition directly expressed in constraints. It has also proven useful for combinations of static and dynamic analysis.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00974764
Contributor : Catherine Oriat <>
Submitted on : Monday, April 7, 2014 - 2:16:27 PM
Last modification on : Friday, June 25, 2021 - 9:52:03 AM

Links full text

Identifiers

Collections

CNRS | CEA | LIG | DRT | LIST | UGA

Citation

Mickaël Delahaye, Nikolai Kosmatov. A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools. Runtime Verification (RV 2013), 2013, Rennes, France. pp.328-333, ⟨10.1007/978-3-642-40787-1_20⟩. ⟨hal-00974764⟩

Share

Metrics

Record views

314