Alessandra Di Pierro and Herbert Wiklicky
- Area: LoCo
- Level: I
- Week: 2
- Time: 17:00 – 18:30
- Room: C3.06
Abstract
This introductory course will be concerned with the probabilistic analysis of deterministic and probabilistic programs, that is on how to obtain, estimate or approximate statistical or probabilistic judgements about certain (quantitative) properties of such programs.
In order to allow for a formal investigation of such features we will first discuss ways to specify or define the semantics of probabilistic programs; in particular to this purpose we will consider Discrete Time Markov Chains. Our focus will then be on Probabilistic Abstract Interpretation (PAI) as a way to obtain simplified or abstract versions of the concrete semantics of programs.
We will introduce the mathematical theory of PAI which is based on linear operators and a notion of pseudo-inverse generalising the one of a Galois connection.
Various static and dynamic analysis techniques based on PAI will be demonstrated by presenting their applications, e.g. in the context of information security, and concrete calculations based on an experimental tool.
We will also discuss how this framework compares with other approaches towards probabilistic semantics (e.g. probabilistic traces and weakest preconditions) and program analysis (such as probabilistic model checking and verification).
