You are here

Home » News » Structuring an Abstract Interpreter through Value and State Abstractions: EVA, an Evolved Value Analysis for Frama-C

Structuring an Abstract Interpreter through Value and State Abstractions: EVA, an Evolved Value Analysis for Frama-C

Submitted by Lydie MABIL on Mon 6 Mar 2017 - 15h48

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 :

The formal verification of programs is nowadays a crucial challenge for computer science, as software bugs in critical systems may lead to catastrophic outcomes. Abstract interpretation is a general theory of approximation of the semantics of programming languages, practically used to detect errors in programs. Automatic analyses can be derived by computing an over-approximation of the possible behav-iors of a program, through abstractions of its concrete semantics.
This thesis proposes a new framework for the combination of multiple abstractions in the abstract interpretation theory. Its core concept is the structuring of the abstract semantics by following the usual distinction between expressions and statements. This can be achieved by a convenient architecture where abstractions are separated in two layers: value abstractions, in charge of the expression semantics, and state abstractions (or abstract domains), in charge of the statement
semantics.
This design leads naturally to an elegant communication system where the abstract states, when interpreting a statement, interact and exchange information through abstract values, that express properties about expressions. While the values form the communication interface between states, they are also standard elements of the abstract interpretation framework. Different kinds of value abstractions can thus be composed through the existing methods of combination of abstractions, enabling even further interactions.
The general system of abstractions combination has been implemented within EVA , the new version of the abstract interpreter provided by the Frama-C platform.
Speaker: 
David Bühler (Celtique)
Department: 
D4 - LANGUAGE AND SOFTWARE ENGINEERING
Date: 
Wednesday, 15. March 2017 - 14:00 to 18:00
Place: 
IRISA Rennes - Salle Michel Métivier
Defense Type: 
Thesis
Composition of jury: 
  • 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.