MILANESE Marco

Doctorant
Équipe : APR
Date d'arrivée : 01/11/2022
    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, Marco.Milanese (at) nulllip6.fr
https://lip6.fr/Marco.Milanese

Direction de recherche : Antoine MINÉ

Analyse sous-approximée et génération de contres-exemples par interprétation abstraite

Le but de la thèse est le développement, la preuve de correction, l'implantation et l'expérimentation de méthodes d'analyse statique de programmes pour découvrir des exécutions garanties formellement d'être incorrectes et, de manière complémentaire, d'inférer automatiquement des pré-conditions suffisantes assurant la correction des programmes.
Le travail s'appuiera sur la théorie de l'interprétation abstraite et proposera de nouvelles abstractions sous-approximantes des états de programme. L'état de l'art en théorie et application de l'interprétation abstraite est essentiellement focalisé sur le calcul de sur-approximations. En cas d'alarme, il n'est pas possible de conclure à la présence d'une erreur réelle, ou celle d'une fausse alarme causée par la sur-approximation. Des analyses arrières ont été proposées pour calculer des pré-conditions nécessaires à la présence d'une erreur, mais elles calculent toujours des sur-approximations, et ne permettent donc pas toujours de conclure. La thèse développera des nouvelles méthodes d'analyse statique en arrière sous-approximante, basées sur l'interprétation abstraite, pour inférer automatiquement des conditions suffisantes pour que certains comportements de programme puissent se produire. L'effort d'implantation et d'expérimentation sera conduit au sein de la plateforme d'analyse statique MOPSA développée dans l'équipe APR du LIP6 à Sorbonne Université.

Publications 2023-2024

Mentions légales
Carte du site