Tout commence par une motivation très concrète : s'assurer que les logiciels font bien ce que l'on attend d'eux ; ou, plus modestement, s'assurer qu'ils ne font pas quelque chose de stupide ou dangereux.
Les obstacles sont de deux ordres :
Il est difficile d'agir sur le second point, qui est un problème humain. Par contre, il est possible d'agir sur le premier point. Il ne s'agit pas d'aller contre une impossibilité mathématique, mais de la contourner. Nous n'essaierons donc pas de produire des méthodes universelles, mais des méthodes qui marcheront raisonnablement sur des programmes raisonnables qui intéressent les utilisateurs. Il s'agira donc de méthodes approximées.
Ceci dit, « approximé » n'implique pas « sans rigueur ». Nous voulons faire des méthodes d'analyse qui soient fiables sans être optimales. Par exemple, nous admettrons qu'un analyseur réponde « le contrôleur informatisé mettra la gouverne de la fusée dans une position comprise entre 0 et 35 degrés », même si en fait cela ne dépassera jamais 33 degrés. Par contre, nous n'accepterons pas qu'il dise quelque chose de faux, par exemple prétendre que la position sera forcément comprise entre 0 et 30 degrés alors qu'elle peut dépasser cette dernière limite.
Sans aller jusqu'aux problèmes de systèmes critiques évoqués ci-dessus, des analyseurs de programmes sont couramment utilisés dans des compilateurs, c'est à dire des logiciels qui transforment un listing lisible par un humain en un programme exécutable par la machine. En effet, cette opération peut se faire plus ou moins astucieusement, et on attend d'un bon compilateur qu'il soit astucieux ! Pour prendre un exemple un peu artificiel, si un compilateur s'aperçoit, par une analyse, qu'un certain nombre n est pair quelle que soit l'utilisation, il est inutile d'émettre un bout de programme pour gérer le cas où il serait impair, lequel ne serait jamais utilisé et gâcherait de l'espace en mémoire, ralentissant en outre le système.
Un problème avec les techniques généralement utilisées jusqu'ici est qu'elles ne prennent pas en compte la probabilité des évènements. Ainsi, elles ne distinguent pas entre un évènement possible avec une grande probabilité et un évènement certes possibles, mais très improbable.
Nous proposons donc des méthodes permettant d'évaluer (en général, de majorer) quantitativement les probabilités de certains évènements. Nous étendons cette analyse aux cas où toutes les particularités statistiques du système ne sont pas connues, rajoutant du non-déterminisme au sens habituel du terme.
Le premier problème posé par la réalisation d'analyseurs statiques de programmes probabilistes est la définition précise d'une sémantique, c'est-à-dire d'une application qui à un programme associe une définition mathématique de « ce qu'il calcule »
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é 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.
| [1] |
David Monniaux.
Abstract interpretation of probabilistic semantics.
In Seventh International Static Analysis Symposium (SAS'00),
number 1824 in Lecture Notes in Computer Science, pages 322-339. Springer
Verlag, 2000.
Extended version on the author's web site.
[ bib |
.ps.gz |
.pdf ]
Following earlier models, we lift standard deterministic and nondeterministic semantics of imperative programs to probabilistic semantics. This semantics allows for random external inputs of known or unknown probability and random number generators. We then propose a method of analysis of programs according to this semantics, in the general framework of abstract interpretation. This method lifts an “ordinary” abstract lattice, for non-probabilistic programs, to one suitable for probabilistic programs. Our construction is highly generic. We discuss the influence of certain parameters on the precision of the analysis, basing ourselves on experimental results.
|
| [2] |
David Monniaux.
An abstract Monte-Carlo method for the analysis of probabilistic
programs (extended abstract).
In 28th Symposium on Principles of Programming Languages (POPL
'01), pages 93-101. Association for Computer Machinery, 2001.
[ bib |
.ps.gz |
.pdf ]
We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. After introducing “ordinary” testing, we show how to combine testing and abstract interpretation and give formulas linking the precision of the results to the number of iterations. We then discuss complexity and optimization issues and end with some experimental results.
|
| [3] |
David Monniaux.
Backwards abstract interpretation of probabilistic programs.
In European Symposium on Programming Languages and Systems (ESOP
'01), number 2028 in Lecture Notes in Computer Science, pages 367-382.
Springer Verlag, 2001.
[ bib |
.ps.gz |
.pdf ]
We introduce an extension of the framework of backwards abstract interpretation to probabilistic programs. This extension is proved to be sound with respect to a semantics that we introduce and prove to be equivalent to the standard semantics of probabilistic programs. We then propose a generic construction lifting ordinary abstract interpretation lattices to probabilistic programs.
|
| [4] |
David Monniaux.
An abstract analysis of the probabilistic termination of programs.
In 8th International Static Analysis Symposium (SAS'01), number
2126 in Lecture Notes in Computer Science, pages 111-126. Springer Verlag,
2001.
[ bib |
.ps.gz |
.pdf ]
It is often useful to introduce probabilistic behavior in programs, either because of the use of internal random generators (probabilistic algorithms), either because of some external devices (networks, physical sensors) with known statistics of behavior. Previous works on probabilistic abstract interpretation have addressed safety properties, but somehow neglected probabilistic termination. In this paper, we propose a method to automatically prove the probabilistic termination of programs using exponential bounds on the tail of the distribution. We apply this method to an example and give some directions as to how to implement it. We also show that this method can also be applied to make unsound statistical methods on average running times sound.
|
| [5] |
David Monniaux.
Analyse de programmes probabilistes par interprétation
abstraite.
Thèse de doctorat, Université Paris IX Dauphine, 2001.
Résumé étendu en francais. Contents in English.
[ bib |
.pdf ]
The 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.
|
| [6] |
David Monniaux.
Abstraction of expectation functions using gaussian distributions.
In Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, and Supratik
Mukhopadhyay, editors, Verification, Model Checking, and Abstract
Interpretation: VMCAI '03, number 2575 in Lecture Notes in Computer Science,
pages 161-173. Springer Verlag, 2003.
[ bib |
.ps.gz |
.pdf ]
We consider semantics of infinite-state programs, both probabilistic and nondeterministic, as expectation functions: for any set of states A, we associate to each program point a function mapping each state to its expectation of starting a trace reaching A. We then compute a safe upper approximation of these functions using abstract interpretation. This computation takes place in an abstract domain of extended Gaussian (normal) distributions.
|
| [7] |
David Monniaux.
Abstract interpretation of programs as Markov decision processes.
In Static Analysis Symposium (SAS '03), number 2694 in Lecture
Notes in Computer Science, pages 237-254. Springer Verlag, 2003.
[ bib |
.ps.gz |
.pdf ]
We propose a formal language for the specification of trace properties of probabilistic, nondeterministic transition systems, encompassing the properties expressible in Linear Time Logic. Those formulas are in general undecidable on infinite deterministic transition systems and thus on infinite Markov decision processes. This language has both a semantics in terms of sets of traces, as well as another semantics in terms of measurable functions; we give and prove theorems linking the two semantics. 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.
|
En outre, les transparents de ma soutenance de thèse sont disponibles.