Macquarie University
01whole.pdf (2.2 MB)

Semantics and loop invariant synthesis for probabilistic programs

Download (2.2 MB)
posted on 2022-03-28, 12:10 authored by Friedrich Gretz
In this thesis we consider sequential probabilistic programs. Such programs are a means to model randomised algorithms in computer science. They facilitate the formal analysis of performance and correctness of algorithms or security aspects of protocols. We develop an operational semantics for probabilistic programs and show it to be equivalent to the expectation transformer semantics due to McIver and Morgan. This connection between the two kinds of semantics provides a deeper understanding of the behaviour of probabilistic programs and is instrumental to transfer results between communities that use transition systems such as Markov decision processes to reason about probabilistic behaviour and communities that focus on deductive verification techniques based on expectation transformers. As a next step, we add the concept of observations and extend both semantics to facilitate the calculation of expectations which are conditioned on the fact that no observation is violated during the program's execution. Our main contribution here is to explore issues that arise with non-terminating, non-deterministic or infeasible programs and provide semantics that are generally applicable. Additionally, we discuss several program transformation to facilitate the understanding of conditioning in probabilistic programming. In the last part of the thesis we turn our attention to the automated verification of probabilistic programs. We are interested in automating inductive verification techniques. As usual the main obstacle in program analysis are loops which require either the calculation of fixed points or the generation of inductive invariants for their analysis. This task, which is already hard for standard, i.e. non-probabilistic, programs, becomes even more challenging as our reasoning becomes quantitative. We focus on a technique to generate quantitative loop invariants from user defined templates. This approach is implemented in a software tool called Prinsys and evaluated on several examples.


Table of Contents

1. Introduction -- 2. Linking operational and denotational semantics -- 3. Conditional probabilities and expectations -- 4. Automated analysis -- Chapter 5. Conclusion and future work -- Appendices.


"A thesis submitted in fulfilment of the requirements for the degree of Doctor of Philosophy in the Department of Computing, Faculty of Science and Engineering, Macquarie University". "2014". Bibliography: pages 75-82

Awarding Institution

Macquarie University

Degree Type

Thesis PhD


PhD, Macquarie University, Faculty of Science and Engineering, Department of Computing

Department, Centre or School

Department of Computing

Year of Award


Principal Supervisor

Annabelle. McIver


Copyright Friedrich Gretz 2015. Copyright disclaimer: Copyright disclaimer:




1 online resource (x, 85 pages) illustrations (some coloured)

Former Identifiers


Usage metrics

    Macquarie University Theses


    Ref. manager