Vérification probabiliste de résultats d'analyse statique

Ce document traite de la vérification probabiliste de résultats d'analyse statique. Il s'agit plus précisément de mettre au point un algorithme de Monte-Carlo permettant de vérifier qu'un objet (appelé certificat) que l'on nous donne est bien le résultat d'une analyse statique. À notre connaissance, aucun algorithme de la sorte n'existe. Nous avons donc commencé par nous définir un cas précis sur lequel travailler à savoir une analyse Points-to sur un langage impératif simple que nous définissons. Nous avons ensuite proposé un algorithme de Monte-Carlo qui soit simple à implémenter et rapide à exécuter pour ce cas en particulier. Une grande partie de notre travail a alors consisté à démontrer que l'algorithme avait de bonnes propriétés de convergence en termes de probabilité d'erreur. Nous avons enfin implémenté cet algorithme afin d'obtenir des résultats expérimentaux. Finalement, nous proposons des pistes pour élargir le champ d'application et ne plus se restreindre à un cas précis