E. Engendrée-par-{pair-de-x-sur-les-valeurs-paires, Formellement, une filtration de F notée (F n ) n?N est une suite de soustribus de F telle que ?n ? N, F n ? F n+1 Par exemple, considérons ? = { population française } et F = P(?) Une filtration peut être la suite de tribus engendrée par ? (F 0 ), { hommes, femmes } (F 1 ), { hommes de moins de 15 ans, hommes de plus de 15 ans, femmes de moins de 15 ans, femmes de plus de 15 ans} (F 2 ) En conditionnant une variable aléatoire par une filtration, on obtient alors une suite variables aléatoires de plus en plus précises. Par exemple soit Y la variable aléatoire qui donne la masse d'un français choisi au hasard On a alors E(Y|F 0 ) qui traduit la masse moyenne des Français, E(Y|F 1 ) qui correspond à une variable donnant soit la masse moyenne des hommes en France soit la masse moyenne des femmes en France, et E(Y|F 2 ) qui ajoute la distinction entre les plus et moins de 15 ans Nous pouvons maintenant définir ce que sont les martingales. Le principe d'une martingale est de modéliser l'évolution d'une variable aléatoire « à mesure que nos connaissances augmenten ». On pose donc une filtration (F n ) n?N qui correspond à l'augmentation des connaissances. En effet, plus n grandit, plus F n grandit et est fine, plus on peut faire des distinctions entre les événements. On pose alors une suite de variables aléatoires (X n ) n?N qui est la valeur que l'on souhaite estimer. On exige que pour tout n, X n est F n mesurable. Cela signifie que l'on connaît la valeur de X n , si l'on a connaissance de F n . Une surmartingale (qui le type de martingale qui nous intéresse) possède de plus la propriété suivante : ?n ? N, X n ? E(X n + 1 | F n ) Cela revient à dire qu'en moyenne la suite (X n ) n?N décroît. Nous allons prendre l'exemple de l'estimation qu'à notre algorithme probabiliste de se tromper. En conclusion, on peut représenter la probabilité qu'a notre algorithme de se tromper par une surmartingale. Nous remarquons que noun n'avons pas utilisé d'hypothèse sur la dépendance entre les relations d'appartenance. De plus, notre preuve ne repose que sur le fait que l'algorithme teste des appartenances. La surmartingale que nous avons définie est donc plus générale que notre algorithme. D'abord, elle peut modéliser un algorithme différent de 1. Ensuite, on peut parfaitement la transposer à une analyse sensible au flot (ou Label {.}, cf. section 4 ) Pour finir, un algorithme de vérification d'un certificat censé être une sémantique collectrice (section 3.4) peut aussi être modélisée par cette même surmartingale. En effet cela consiste à tester que des ensembles d'ensembles sont inclus les uns dans les autres. Ces tests peuvent être modélisés de manière atomique par plusieurs tests d'appartenance. Un intérêt des martingales, outre un cadre général est l'existence d'outils mathématiques permettant de borner (voire calculer) la vitesse de convergence. Dans le cas de notre martingale, il est évident que (X n ) n?N converge vers 0 après un nombre inifini d'étapes (car il y a un nombre fini d'appartenance à vérifier) On peut cependant se demander à partir de quelle étape on a X n ? 0.05 par expemple. La théorie des martingales propose un outil pour cela : le temps d'arrêt. Intuitivement, le temps d, On peut définir la variable aléatoire qui donne le numéro de l'étape ou le temps d'arrêt advient. La théorie des martingales fournit des outils pour calculer la loi de cette variable aléatoire. Maintenant que nous avons une possible amélioration de l'approche théorique

. La-constante-est, un bit par valeur plutôt que la taille d'un entier (32 bits le plus souvent) 11 http ://sawja.inria.fr/ 8 Conclusion Pour conclure, nous avons, à notre connaissance, réalisé le premier algorithme de vérification d'un certificat par rapport à une analyse statique. Nous sommes, pour ce faire, placé dans un sous-contexte précis que nous maitrisions afin de pouvoir acquérir une meilleure connaissance de la problématique. De plus, nous avons implémenté notre solution pour ne pas perdre vue l'objectif applicatif que nous avons. L'implémentation a été testée et les premiers résultats sont encourageants bien que du travail puisse encore être fait en termes de complexité temporelle et de pertinences des équations testées. De plus, nous sommes maintenant en mesure de proposer des axes de recherche plus généraux afin de ne plus avoir s'astreindre au sous-problème que nous nous sommes posé, Nous estimons que l'utilisation de martingales

R. Gall, Intégration, probabilités, processus aléatoires

[. Gulwani and G. C. Necula, Discovering affine equalities using random interpretation, 30 th Annual Symposium ACM on Principles of Programming Langages, pp.74-84, 2003.

S. Gulwani and G. C. Necula, Global value numbering using random interpretation, 31 st Annual Symposium ACM on Principles of Programming Langages, pp.342-352, 2004.

S. Gulwani and G. C. Necula, A polynomial-time algorithm for global value numbering Precise interprocedural analysis using random interpretation, 11 th Static Analysis Symposium 32 nd Annual Symposium ACM on Principles of Programming Langages, pp.212-227, 2004.

S. Gulwani, Program analysis using random interpretation, 2005.

R. Motwani and P. Raghavan, Randomized algorithms, 1995.

[. Nasre and R. Govindarajan, Points-to Analysis as a System of Linear Equations, In Lecture Notes in Computer Science, vol.6337, pp.422-438, 2011.
DOI : 10.1007/978-3-642-15769-1_26

J. Whaley, D. Avots, M. Carbin, and M. S. Lam, Using Datalog with Binary Decision Diagrams for Program Analysis, In Lecture Notes in Computer Science, vol.3780, pp.98-118, 2005.
DOI : 10.1007/11575467_8

J. Whaley and M. S. Lam, Cloning-based context sensitive pointer alias analysis using binary decision diagrams, conference on Programming language Design and Implementation, 2004.