Amphithéâtre - Maison Jean Kuntzmann
13 octobre 2014 - 15h30
Analyse statique de programmes par interprétation abstraite et procédures de décision (Phd Defense)
par Julien Henry de Université de Grenoble
Résumé : Chers tous,
J'ai le plaisir de vous inviter à la soutenance de ma thèse de doctorat, intitulée:
Analyse statique de programmes par interprétation abstraite et procédures de décision
qui aula lieu le lundi 13 octobre 2014 à 15h30 dans l'amphithéâtre de la Maison Jean Kuntzmann. Un plan d'accès est disponible à l'adresse http://mi2s.imag.fr/plans-dacces .
Vous êtes également cordialement conviés au pot de thèse qui suivra.
Résumé:
L'analyse statique de programme a pour but de prouver automatiquement qu'un programme vérifie certaines propriétés. L'interprétation abstraite est un cadre théorique permettant de calculer des invariants de programme. Ces invariants sont des propriétés sur les variables du programme vraies pour toute exécution. La précision des invariants calculés dépend de nombreux paramètres, en particulier du domaine abstrait et de l'ordre d'itération utilisés pendant le calcul d'invariants.
Dans cette thèse, nous proposons plusieurs extensions de cette méthode qui améliorent la précision de l'analyse.
Habituellement, l'interprétation abstraite consiste en un calcul de point fixe d'un opérateur obtenu après convergence d'une séquence ascendante, utilisant un opérateur appelé élargissement. Le point fixe obtenu est alors un invariant. Il est ensuite possible d'améliorer cet invariant via une séquence descendante sans élargissement. Nous proposons une méthode pour améliorer un point fixe après la séquence descendante, en recommençant une nouvelle séquence depuis une valeur initiale choisie judiscieusement.
L'interprétation abstraite peut également être rendue plus précise en distinguant tous les chemins d'exécution du programme, au prix d'une explosion exponentielle de la complexité. Le problème de satisfiabilité modulo théorie (SMT), dont les techniques de résolution ont été grandement améliorée cette décennie, permettent de représenter ces ensembles de chemins implicitement. Nous proposons d'utiliser cette représentation implicite à base de SMT et de les appliquer à des ordres d'itération de l'état de l'art pour obtenir des analyses plus précises.
Nous proposons ensuite de coupler SMT et interprétation abstraite au sein de nouveaux algorithmes appelés Modular Path Focusing et Property-Guided Path Focusing, qui calculent des résumés de boucles et de fonctions de façon modulaire, guidés par des traces d'erreur. Notre technique a différents usages: elle permet de montrer qu'un état d'erreur est inatteignable, mais également d'inférer des préconditions aux boucles et aux fonctions.
Nous appliquons nos méthodes d'analyse statique à l'estimation du temps d'exécution pire cas (WCET). Dans un premier temps, nous présentons la façon d'exprimer ce problème comme un problème d'optimisation modulo théorie, et pourquoi un encodage naturel du problème en SMT génère des formules trop difficiles pour l'ensemble des solveurs actuels. Nous proposons un moyen simple et efficace de réduire considérablement le temps de calcul des solveurs SMT en ajoutant aux formules certaines propriétés impliquées obtenues par analyse statique.
Enfin, nous présentons l'implémentation de Pagai, un nouvel analyseur statique pour LLVM, qui calcule des invariants numériques grâce aux différentes méthodes décrites dans cette thèse. Nous avons comparé les différentes techniques implémentées sur des programmes open-source et des benchmarks utilisés par la communauté.
Jury:
Prof. Cesare Tinelli University of Iowa, Rapporteur
Dr. Antoine Miné Ecole Normale Supérieure, Rapporteur
Dr. Hugues Cassé Université de Toulouse - IRIT, Examinateur
Prof. Roland Groz Grenoble-INP, Examinateur
Prof. Andreas Podelski University of Freiburg, Examinateur
Dr. David Monniaux CNRS - Verimag, Directeur de Thèse
Dr. Matthieu Moy Grenoble-INP - Verimag, Co-Encadrant de Thèse
