Advanced Weakest Precondition Calculi for Probabilistic Programs
My research aims at developing techniques for the automated analysis of probabilistic programs. These kind of programs are of great importance in fields such as security, quantum computing, randomized algorithms and machine learning, where Bayesian inference is needed for the analysis.
While probabilistic programs, for instance in their occurrence in security protocols, mostly consist of only a few lines of code, their underlying semantics is given by infinite systems such as Markov decision processes which makes the verification of certain probabilities very hard or even undecidable. We study decidability questions and explore possibilities of automated analysis techniques given the fact that we have to handle infinite domains in combination with arbitrary parameters. This is done by means of identifying reasonable sub-classes, where results on the underlying semantics can be used, as well as by developing new techniques.