Ce papier, écrit avec P. Cousot, propose un nouveau formalisme pour analyser statiquement des programmes à interactions probabilistes, qui étend le cadre habituel de l'interprétation abstraite. Il a été publié à ESOP 2012.

Ci-dessous le papier et une version étendue (ie. avec preuves et introduction), ainsi que certaines des présentations qui en ont été faites pour expliciter les intuitions.

• Probabilistic Abstract Interpretation, ESOP 2012 paper, BibTeX file.
• Probabilistic Abstract Interpretation, extended version.
• Présentations :
  • Version courte : ESOP 2012.
  • Version plus détaillée : faite au MIT et à Microsoft Research en 2011.

Présentation au séminaire NEVER à NYU - travail à l'Imperial College avec Chris Hankin.

Description d'un nouveau framework pour prédire statiquement le contenu du cache à l'exécution du programme. Ce nouveau domaine abstrait est modulaire et permet d'interchanger stratégies de remplacement et hiérachies, et s'applique donc facilement (et automatiquement) à toutes les configurations pratiques. (Le papier plus précis est en cours d'écriture.)

Téléchargement

C'est le rapport du stage chez Microsoft Research à Redmond que j'ai fait pendant l'été 2009. Ce travail s'intéresse à une technique développée pour faire persister les contrats inférés lors d'analyses par interprétation abstraite, ainsi qu'à l'implémentation d'analyses d'objets dans Clousot, l'analyseur statique pour les langages .NET développé à Microsoft Research.

Téléchargement, Download

Réalisé dans le cadre d'un groupe de travail sur le théorème PCP à l'ENS, ce document traite de la génération automatique de "gadgets" pour réduire des problèmes algorithmiques usuels (par exemple MaxCut) à d'autres. Quelques résultats en relation avec le théorème PCP sont énoncés mais tous ne sont pas prouvés.

Téléchargement

On étudie ici la manière dont les monades, venues directement de la théorie des catégories, permettent de simuler des comportements impératifs dans un cadre de programmation purement fonctionnelle. On illustre tout ceci en Haskell.

Téléchargement

L'objectif de cette étude est de comprendre la manière dont le modèle de l'ordinateur quantique permet d'accélérer de manière exponentielle des algorithmes classiques, avec en contrepartie une faible probabilité d'échec. Y sont traités les algorithmes de Shor et (brièvement) de Grover.

Téléchargement

Réalisé avec Arnaud de Mesmay dans le cadre du mémoire de M1, ce travail s'intéresse à la résolution approchée des problèmes (liés) Sparsest Cut et Multicommodity flow

Pour ceci, on étudie des propriétés géométriques des graphes en les plongeant (avec distorsion) dans des espaces , puis en leur appliquant des résultats issus de géométrie discrète. En particulier, nous traitons de récents développements dans le domaine dus à Linial, London et Rabinovich, ainsi que certaines améliorations qui ont été par la suite apportées à leurs résultats.

PDF du rapport & Binaires zippés du programme réalisé (voir rapport) - fonctionne sous Windows et en OpenGL)

On s'intéresse ici à un récent théorème en théorie de la décidabilité : le théorème de cardinalité (Kummer, 1992).

PDF du rapport & Présentation orale

L'objectif est d'étudier de manière précise un certain nombre d'outils et de résultats de géométrie différentielle qui tendent à formaliser l'idée que certaines situations ou relations entre objets sont omniprésentes (on dira génériques). Précisément, on s'intéresse au théorème de transversalité de René Thom qui donne un moyen très pratique de montrer la généricité de certaines propriétés. On applique ensuite ces résultats aux fonctions de Morse.

Téléchargement c'est mon TIPE de 5/2 en version longue.

Ce travail s'attache à caractériser les systèmes dynamiques linéaires dont les trajectoires intégrales se "ressemblent". Cela mène naturellement à la classification des endomorphismes de par conjugaison. On résout donc ce problème dans le cas (générique) des endomorphismes hyperboliques, puis on étudie le théorème de Großman-Hartman qui montre que l'étude linéaire réalisée jusque là peut s'étendre dans une certaine mesure au cas non-linéaire.

Téléchargement c'est mon TIPE de 3/2.