In this thesis we consider sequential probabilistic programs. Such programsare a means to model randomised algorithms in computer science. They facilitatethe formal analysis of performance and correctness of algorithms or securityaspects of protocols.We develop an operational semantics for probabilistic programs and showit to be equivalent to the expectation transformer semantics due to McIver andMorgan. This connection between the two kinds of semantics provides a deeperunderstanding of the behaviour of probabilistic programs and is instrumental totransfer results between communities that use transition systems such as Markovdecision processes to reason about probabilistic behaviour and communities thatfocus on deductive verification techniques based on expectation transformers.As a next step, we add the concept of observations and extend both semanticsto facilitate the calculation of expectations which are conditioned on the fact thatno observation is violated during the program’s execution. Our main contributionhere is to explore issues that arise with non-terminating, non-deterministic or infeasibleprograms and provide semantics that are generally applicable. Additionally,we discuss several program transformations to facilitate the understandingof conditioning in probabilistic programming.In the last part of the thesis we turn our attention to the automated verificationof probabilistic programs. We are interested in automating inductive verificationtechniques. As usual the main obstacle in program analysis are loopswhich require either the calculation of fixed points or the generation of inductiveinvariants for their analysis. This task, which is already hard for standard, i.e.non-probabilistic, programs, becomes even more challenging as our reasoningbecomes quantitative. We focus on a technique to generate quantitative loop invariantsfrom user defined templates. This approach is implemented in a softwaretool called Prinsys and evaluated on several examples.
展开▼
