Explanation-based generalization of infeasible path

Mickaël Delahaye 1 Bernard Botella 1 Arnaud Gotlieb 2
2 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Recent code-based test input generators based on dynamic symbolic execution increase path coverage by solving path condition with a constraint or an SMT solver. When the solver considers path condition produced from an infeasible path, it tries to show unsatisfiability, which is a useless timeconsuming process. In this paper, we propose a new method that takes opportunity of the detection of a single infeasible path to generalize to a (possibly infinite) family of infeasible paths, which will not have to be considered in further path conditions solving. The method exploits non-intrusive constraint-based explanations, a technique developed in Constraint Programming to explain unsatisfiability. Experimental results obtained with our prototype tool IPEG show that, whatever is the underlying constraint solving procedure (IC, Colibri and the SMT solver Z3), this approach can save considerable computational time.
Type de document :
Communication dans un congrès
3rd IEEE International Conference on Software Testing, Validation and Verification (ICST'10), Apr 2010, Paris, France. 2010
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00699240
Contributeur : Arnaud Gotlieb <>
Soumis le : lundi 21 mai 2012 - 11:09:24
Dernière modification le : jeudi 15 novembre 2018 - 11:57:41
Document(s) archivé(s) le : vendredi 30 novembre 2012 - 11:57:10

Fichier

paper2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00699240, version 1

Citation

Mickaël Delahaye, Bernard Botella, Arnaud Gotlieb. Explanation-based generalization of infeasible path. 3rd IEEE International Conference on Software Testing, Validation and Verification (ICST'10), Apr 2010, Paris, France. 2010. 〈hal-00699240〉

Partager

Métriques

Consultations de la notice

348

Téléchargements de fichiers

261