All begins by a very concrete motivation: ensuring that programs do what the user wants them to do; or, more modestly, ensure that they won't do something stupid or dangerous.
Obstacles are twofold:
Working against the second point is difficult, since it is a human problem. On the other hand, working against the first is possible. We do not wish to break through some mathematical impossibility, but to work around it. We do not wish to design universal methods, but methods that work reasonably well on reasonable programs that interest actual users. We shall therefore deal with approximations.
Approximation does not imply an absence of rigor. We wish to make analysis methods that are reliable without being optimal. For instance, we shall allow an analyser to answer "the computer that drives the rocket's deflector will set it between 0 and 35 degrees", even though this position will never go further than 33 degrees. On the other hand, we shall not accept that it says something false, for instance pretend that the position shall always be between 0 and 30 degrees whereas it can go further this limit.
Without going to problems of critical systems such as the ones cited above, program analysers are currently used in compilers, that is, programs that turn a human-readable program listing into machine-executable code. This operation can indeed be done more or less cleverly, and cleverness is expected from good compilers. To take a somewhat artificial example, if a compiler notices, after an analysis, that some n is even however the program is used, emitting code to handle the case it is odd is unneccessary, since such code would never be used and waste memory space, furthermore slowing down the system.
A problem with the techniques generally used up to now is that they don't take the probability of events into account. They don't distinguish between some possible and even probable event and an event that is, although possible, very improbable.
Nous proposons donc des méthodes permettant d'évaluer (en général, de majorer) quantitativement les probabilités de certains évènements. We extend this analysis to cases where all the statistical pecularities of the system are not know, adding nondeterminism in the classical sense.
The first problem when building static analyzers for probabilistic programs is the precise definition of a semantics, mapping a program to a mathematical definition of "what it computes".
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.
| [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.
|
Furthermore, the slides of my PhD dissertation are also available.