You are here
Structuring an Abstract Interpreter through Value and State Abstractions: EVA, an Evolved Value Analysis for Frama-C
Elle sera effectuée en français, et sera suivie d'un pot en salle Sein auquel vous êtes chaleureusement conviés.
Résumé :
La vérification formelle de programmes est devenue un enjeu majeur de l'informatique, à l'heure où des erreurs logicielles dans des secteurs critiques peuvent avoir des conséquences dramatiques. L'interprétation abstraite est une théorie générale d'approximation des sémantiques des langages de programmation, qui permet des analyses automatiques de programmes pour en détecter de façon certaine les comportements indésirables. Ces analyses statiques reposent sur des
abstractions d'une sémantique concrète, qui calculent une sur-approximation des comportements possibles d'un programme.
Cette thèse propose une nouvelle technique de composition modulaire entre les abstractions d'un interpréteur abstrait. L'idée principale en est l'organisation d'une sémantique abstraite suivant la distinction usuelle entre expressions et instructions : les abstractions sont séparées entre abstractions de valeurs, en charge de la sémantique des expressions, et les abstractions d'états, en charge de la sémantique des instructions. Lors de l'interprétation d'une instruction, les états abstraits peuvent échanger des informations au moyen de valeurs abstraites, qui expriment des propriétés sur les expressions. Les valeurs abstraites, en tant qu'éléments canoniques de l'interprétation abstraite, peuvent elle-mêmes être composées par les techniques existantes. Notre
architecture comprend également une collaboration directe des différentes abstractions à l'émission des alarmes qui signalent les erreurs possibles d'un programme.
Ce système de composition des abstractions a été mis en œuvre dans EVA, la nouvelle version de l'interpréteur abstrait de la plateforme Frama-C.
Abstract :
- Antoine Miné, Professeur des Universités à l'Université Pierre et Marie Curie, rapporteur ;
- Mihaela Sighireanu, Maître de Conférences à l'Université Paris Diderot, rapporteur ;
- Thomas Jensen, Directeur de Recherche à Inria Rennes, examinateur ;
- Yann Régis-Gianas, Maître de Conférences à l'Université Paris Diderot, examinateur ;
- Sandrine Blazy, Professeur des Universités à l'Université de Rennes 1, directrice de thèse ;
- Boris Yakobowski, Ingénieur Chercheur au CEA LIST, co-directeur de thèse.