LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Actualité » Doctorants

JOURNAULT Matthieu

Docteur (ATER, )
Équipe : APR
Localisation : Campus Pierre et Marie Curie
    Sorbonne Université - LIP6
    Boîte courrier 169
    Couloir 25-26, Étage 3, Bureau 303
    4 place Jussieu
    75252 PARIS CEDEX 05
Tel: 01 44 27 88 16, Matthieu.Journault (at) nulllip6.fr
https://www-apr.lip6.fr/~journault/
Direction de recherche : Antoine MINÉ

Analyse statique modulaire précise par interprétation abstraite pour la preuve automatique de correction de programmes et pour l’inférence de contrats

Assurer le passage à l’échelle des analyseurs statiques définis par interprétation abstraite pose des difficultés. Une méthode classique d’accélération consiste en la découverte et la réutilisation de contrats satisfaits par certaines commandes du code source. Cette thèse s’intéresse à un sous-ensemble de C qui ne permet pas la récursivité, pour lequel on définit un analyseur modulaire capable d’inférer, de prouver et d'exploiter de tels contrats.
Notre analyse est défini au-dessus d’un analyseur C existant et est donc capable de manipuler des types unions, des types structures, des tableaux, des allocations de mémoire (statique et dynamique), des pointeurs, y compris l'arithmétique de pointeur et le transtypage, appels de fonction, des chaînes de caractères .... La représentation des chaînes de caractère est gérée par un nouveau domaine abstrait défini dans cette thèse.
Nous proposons de plus une technique paramétrique de transformation de la sémantique classique des domaines abstraits vers une sémantique d’ensembles hétérogènes. Cette technique ne maintient qu’un seul état abstrait numérique, par opposition au partitionnement.
Finalement, nous proposons un domaine abstrait capable de représenter des ensembles d’arbres dont les feuilles peuvent contenir des labels numériques. Cette abstraction est basée sur les langages réguliers (d'arbre), et délègue une partie de son abstraction à un domaine numérique sous-jacent.
Cette thèse s’étant déroulée au sein du projet Mopsa, nous donnons donc un aperçu de certains résultats obtenus par l’équipe pendant la thèse.
Soutenance : 21/11/2019 - 14h - Campus Jussieu, salle 24-34/201
Membres du jury :
Mme. BLAZY Sandrine (Professeur, IRISA) [rapporteur]
M. KING Andy (Professeur, University of Kent) [rapporteur]
M. CHAILLOUX Emmanuel (Professeur, Sorbonne Université)
M. LE GALL Tristan (Chercheur, CEA LIST)
M. SOTIN Pascal (Maître de Conférences, IRIT)
M. MINÉ Antoine (Professeur, Sorbonne Université)

Publications 2016-2020

 Mentions légales
Carte du site |