Combinaison de sous et surapproximations de la memoire pour lapos;analyse de code bas-niveau

Description de l'offre : Le théorème de Rice énonçant quapos;on ne peut pas avoir de méthode qui sache automatiquement dire si une propriété sur un programme est vraie ou non a conduit à séparer les outils de vérification en deux groupes: les outils sound fonctionnant par sur-approximation, comme lapos;interprétation abstraite, sont capables de prouver automatiquement que certaines propriétés sont vraies, mais ne savent parfois pas conclure et produisent des alarmes; à lapos;inverse, les outils complete fonctionnant par sous-approximation, comme lapos;exécution symbolique, savent produire des contre-exemples, mais pas démontrer si une propriété est vraie. *Le but général de la thèse est dapos;étudier la combinaison entre méthodes sound et complete dapos;analyse de programme, et en particulier lapos;analyse statique par interprétation abstraite et la génération de formules sous-approximée par exécution symbolique*. Nous nous intéresserons particulièrement à la combinaison dapos;abstractions sur et sous-approximantes, en particulier pour la mémoire. Les applications envisagées en priorité concernent les analyses de code au niveau binaire, telles que réalisées par la combinaison des plateformes dapos;analyse BINSEC et CODEX, pour pouvoir trouver des failles de securite automatiquement ou demontrer leur absence.