A Generic Framework for Symbolic Execution:Theory and Applications: Theory and Applications

Andrei Arusoaie 1, 2
1 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Résumé : L’exécution symbolique représente l’une des techniques les plus populaires utilisées pour l’analyse des programmes. Elle a été employée notamment pour générer des tests de manière automatique ; en plus, elle comporte de nombreuses applications (ex. : la vérification des programmes, le dépannage des programmes, etc.).La thèse de doctorat qui porte le titre « Une approche indépendante du langage de l’exécution symbolique : théorie et applications » présente le cadre générique pour l’exécution symbolique, où le caractère générique est donné par le fait que ce cadre est fondé sur les définitions formelles des langages de programmation. Cela représente un avantage, parce que l’exécution symbolique est implémentée au niveau de la définition du langage de programmation et n’est pas fondée sur la syntaxe ou sur le compilateur d’un certain langage. Dans cette thèse, le cadre d’exécution symbolique est présenté formellement, en utilisant des spécifications algébriques. Cela permet la démonstration de certaines propriétés importantes de l’exécution symbolique :- Coverage : à chaque exécution concrète correspond une exécution symbolique sur le même chemin (d’exécution) du programme.- Precision : à chaque exécution symbolique correspond une exécution concrète sur le même chemin (d’exécution) du programme.Ces deux propriétés sont importantes parce que, au cas où l’on obtient certains résultats qui font référence aux exécutions symboliques, après avoir analysé un programme, elles aident à ce que les résultats puissent être transférés correctement aux exécutions concrètes. En plus, grâce à ces propriétés, le cadre d’exécution symbolique que nous proposons peut être utilisé pour la vérification des programmes.ContributionsLes contributions majeures de cette thèse de doctorat sont :1. Un cadre formel pour l’exécution symbolique et une implémentation de celui-ci, fondé sur la sémantique opérationnelle des langages de programmation :- dans la partie théorique, nous définissons formellement les langages de programmation et l’exécution symbolique ; ensuite, nous démontrons formellement les propriétés Coverage et Precision ;- dans la partie pratique, nous présentons un prototype de ce cadre symbolique, qui est implémenté dans l’environnement pour les définitions de langages K, et qui est fondé sur des transformations de langages ;2. Applications de l’exécution symbolique dans la vérification de programmes :- la vérification de programmes fondée sur la logique Hoare ; dans ce cadre, nous présentons la manière dont on peut utiliser l’exécution symbolique, afin de vérifier des triplets Hoare pour un langage de programmation donné ;- la vérification de programmes fondée sur Reachability Logic ; dans ce cadre, nous présentons un système de déduction alternatif à celui du Reachability Logic, tout comme une stratégie d’application des règles de déduction, qui puisse permettre l’automatisation de la vérification des formules du Reachability Logic ; pour ce système déductif et pour la stratégie proposée, nous avons implémenté un prototype et nous en avons démontré la consistance (fondée sur la consistance du système déductif de Reachability Logic) et une forme de complétude faible (afin de démontrer le caractère faux des formules).
Type de document :
Thèse
Computer Science [cs]. Alexandru Ioan Cuza, University of Iasi, 2014. English
Liste complète des métadonnées

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

https://hal.inria.fr/tel-01094765
Contributeur : Pal Dream <>
Soumis le : mardi 13 janvier 2015 - 11:22:40
Dernière modification le : jeudi 11 janvier 2018 - 02:02:32
Document(s) archivé(s) le : jeudi 10 septembre 2015 - 23:35:27

Identifiants

  • HAL Id : tel-01094765, version 1

Collections

Citation

Andrei Arusoaie. A Generic Framework for Symbolic Execution:Theory and Applications: Theory and Applications. Computer Science [cs]. Alexandru Ioan Cuza, University of Iasi, 2014. English. 〈tel-01094765〉

Partager

Métriques

Consultations de la notice

299

Téléchargements de fichiers

461