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

Mickaël Delahaye 1 Nikolai Kosmatov 2
1 LIG Laboratoire d'Informatique de Grenoble - VASCO
LIG - Laboratoire d'Informatique de Grenoble
2 LSL - Laboratoire Sûreté des Logiciels
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
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.
Type de document :
Communication dans un congrès
Runtime Verification (RV 2013), 2013, Rennes, France. 8174, pp.328-333, 2013, LNCS. 〈10.1007/978-3-642-40787-1_20〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00974764
Contributeur : Catherine Oriat <>
Soumis le : lundi 7 avril 2014 - 14:16:27
Dernière modification le : jeudi 11 janvier 2018 - 01:49:06

Identifiants

Collections

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. 8174, pp.328-333, 2013, LNCS. 〈10.1007/978-3-642-40787-1_20〉. 〈hal-00974764〉

Partager

Métriques

Consultations de la notice

121