Vérification probabiliste de résultats d'analyse statique - DUMAS - Dépôt Universitaire de Mémoires Après Soutenance
Master Thesis Year : 2012

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

Abstract

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.
Fichier principal
Vignette du fichier
Bride.pdf (184.68 Ko) Télécharger le fichier
Loading...

Dates and versions

dumas-00725213 , version 1 (24-08-2012)

Identifiers

  • HAL Id : dumas-00725213 , version 1

Cite

Antoine Bride. Vérification probabiliste de résultats d'analyse statique. Informatique et langage [cs.CL]. 2012. ⟨dumas-00725213⟩
285 View
239 Download

Share

More