Généralisation de chemins infaisables pour l'exécution symbolique
Institution:
Rennes 1Disciplines:
Directors:
Abstract EN:
Software verification is nowadays unavoidable due to the inherent ubiquity and complexity of current software systems. As testing is the primary mean of software verification, automating this task is important. Symbolic execution is the base of numerous tools and techniques to generate automatically test inputs. Symbolic execution inspects program code and, as such, is particularly sensitive to infeasible paths, for which no test input exists. When confronted to such a path, symbolic execution proves that the path is indeed infeasible. This is a waste of time for test input generation. This thesis presents a method to generalize infeasible paths and an integration of this method into test input generation. From a known infeasible path, this method computes a (possibly infinite) family of infeasible paths. Since infeasible paths are often similar, this method finds the reason a path is infeasible and infers a family of paths that are infeasible for the same reason. This method was integrated into a test input generation process that combines symbolic and concrete execution of the program under test, called dynamic symbolic execution. A prototype was developed to evaluate this approach experimentally. Experimental results show that generalization infers path infeasibility more efficiently than symbolic execution and that the speed of test input generation may be improved by this method.
Abstract FR:
La vérification du logiciel est désormais incontournable de par l'ubiquité et la complexité des systèmes informatiques. Le test étant la pratique de vérification la plus courante, son automatisation est intéressante. L'exécution symbolique est une technique à la base de nombreux outils et méthodes de génération automatique de données de test. Inspectant le code des programmes, cette technique est sensible aux nombres de chemins infaisables, pour lesquels aucune donnée de test n'existe. Lorsque l'exécution symbolique rencontre un tel chemin, elle prouve le chemin infaisable ce qui est une perte de temps vis-à-vis de la génération de tests. Cette thèse présente une méthode de généralisation de chemins infaisables et son intégration à la génération de données de test. À partir d'un chemin infaisable découvert par exemple par la génération de données de test, cette méthode calcule une famille (potentiellement infinie) de chemins infaisables. Parce que les chemins infaisables sont souvent similaires, la méthode recherche la raison de l'infaisabilité du chemin considéré et trouve une famille de chemins dont l'infaisabilité découle de cette même raison. Cette méthode a été intégrée dans un processus de génération de tests, qui combine exécution symbolique et exécution concrète du programme sous test, appelé exécution symbolique dynamique. Un prototype a été développé pour évaluer cette approche expérimentalement. Cette évaluation indique que la généralisation déduit des chemins infaisables plus rapidement que l'exécution symbolique et que la génération de données de test est bien accélérée par cette méthode.