Analyse de programmes probabilistes par interprétation abstraite

version corrigée de quelques scoriesThe study of probabilistic programs is of considerable interest for the validation of networking protocols, embedded systems, or simply for compiling optimizations. It is also a difficult matter, due to the undecidability of properties on infinite-state deterministic programs, as well as the difficulties arising from probabilistic aspects.In this thesis, we propose a formulaic language for the specification of trace properties of probabilistic, nondeterministic transition systems, encompassing those that can be specified using deterministic Büchi automata. Those properties are in general undecidable on infinite processes.This language has both a concrete semantics in terms of sets of traces, as well as an abstract semantics in terms of measurable functions. We then apply abstract interpretation-based techniques to give upper bounds on the worst-case probability of the studied property. We propose an enhancement of this technique when the state space is partitioned — for instance along the program points —, allowing the use of faster iteration methods. We propose two abstract domains suitable for this analysis, one parameterized by an abstract domain suitable for nondeterministic (but not probabilistic) abstract interpretation, one modeling extended normal distributions.An alternative method to get such upper bounds works is to apply forward abstract interpretation on measures. We propose two abstract domains suitable for this analysis, one parameterized by an abstract domain suitable for nondeterministic abstract interpretation, one modeling sub-exponential queues. This latter domain allows proving probabilistic termination of programs.The methods described so far are symbolic and do not make use of the statistical properties of probabilities. On the other hand, a well-known way to obtain informations on probabilistic distributions is the Monte-Carlo method. We propose an abstract Monte-Carlo method featuring randomized abstract interpreters.L'étude de programmes probabilistes intéresse plusieurs domaines de l'informatique : les réseaux, l'embarqué, ou encore la compilation optimisée. C'est tâche malaisée, en raison de l'indécidabilité des propriétés sur les programmes déterministes à états infinis, en plus des difficultés provenant des aspects probabilistes.Dans cette thèse, nous proposons un langage de formules permettant de spécifier des propriétés de traces de systèmes de transition probabilistes et non-déterministes, englobant celles spécifiables par des automates de Büchi déterministes. Ces propriétés sont en général indécidables sur des processus infinis.Ce langage a à la fois une sémantique concrète en termes d'ensembles de traces et une sémantique abstraite en termes de fonctions mesurables. Nous appliquons ensuite des techniques d'interprétation abstraite pour calculer un majorant de la probabilité dans le pire cas de la propriété étudiée et donnons une amélioration de cette technique lorsque l'espace d'états est partitionné, par exemple selon les points de programme. Nous proposons deux domaines abstraits convenant pour cette analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les gaussiennes étendues.Il est également possible d'obtenir de tels majorants par des calculs propageant les mesures de probabilité en avant. Nous donnons une méthode d'interprétation abstraite pour analyser une classe de formules de cette façon et proposons deux domaines abstraits adaptés à ce type d'analyse, l'un paramétré par un domaine abstrait non probabiliste, l'autre modélisant les queues sous-exponentielles. Ce dernier permet de prouver la terminaison probabiliste de programmes.Les méthodes décrites ci-dessus sont symboliques et ne tirent pas parti des propriétés statistiques des probabilités. Nous proposons d'autre part une méthode de Monte-Carlo abstrait, utilisant des interpréteurs abstraits randomisés