A Late Treatment of C Precondition in Dynamic Symbolic Execution

Mickaël Delahaye 1 Nikolai Kosmatov 2
1 VASCO
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.
Keywords : test input generation dynamic symbolic execution concolic testing executable preconditions
Type de document :
Communication dans un congrès
CSTVA 2013 - 5th International Workshop on Constraints in Software Testing, Verification, and Analysis, Aug 2013, Luxembourg, Luxembourg. IEEE, pp.230-231, 2013, Proceedings of the IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2013). 〈10.1109/ICSTW.2013.34〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00853725
Contributeur : Mickaël Delahaye <>
Soumis le : vendredi 23 août 2013 - 19:36:47
Dernière modification le : vendredi 16 mars 2018 - 01:12:46

Identifiants

Collections

CEA | LIG_GLSI | LIG_GLSI_VASCO | LIG | UGA | DRT | LIG_SRCPR | LIST

Citation

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. IEEE, pp.230-231, 2013, Proceedings of the IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops (ICSTW 2013). 〈10.1109/ICSTW.2013.34〉. 〈hal-00853725〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

190

Contact


archive-ouverte@inria.fr