Probabilistic programs are sequential programs, written in languages like C, Java, LISP, or ML, with two added constructs: the ability to draw values at random from probability distributions, and the ability to condition values of variables in a program through observations. A variety of probabilistic programming languages has been defined.

Whereas program analysis, either by model checking, theorem proving, or static analysis, for ordinary programs has been well investigated, the formal analysis of probabilistic programs is in its infancy. This holds in particular for termination analysis. Termination analysis is one of the most important aspects of program verification and huge advances toward automated termination proofs of realistic programs have been achieved in the last decades. For probabilistic programs, the corresponding notions are almost-sure termination (i.e., termination with probability one) and positive almost-sure termination, which additionally requires that the expected run-time until the program terminates is finite. Analysing (positive) almost-sure termination is a true challenge—it is provably harder than ordinary program termination.

Most existing approaches to prove almost-sure termination either transform probabilistic programs to non-probabilistic programs or adapt termination techniques like ranking functions to the probabilistic setting. However, the application of ranking functions is only one of the most basic techniques for termination analysis. Based on ranking functions, many further termination techniques can be used which increase the power of automated termination analysis substantially.

A successful approach for termination analysis of non-probabilistic programs is to automatically transform the program into an intermediate representation (e.g., integer term rewrite systems or integer transition systems) and to analyse termination of the resulting system. This has been applied successfully to programming languages such as Java, C, Haskell, and Prolog. The tool AProVE has won several termination competitions in the past years by exploiting these techniques. The next step is to carry this over to probabilistic programs. This dissertation project aims at extending transformation-based termination techniques to obtain a fully automated analysis of (positive) almost-sure termination of probabilistic programs. These techniques will be extended so as to treat dynamic data types (such as lists and trees) exploiting techniques from the literature. Using a prototypical implementation in the termination tool AProVE, extensive experiments will be conducted to evaluate the approach.

(This dissertation project is related to the projects VE4 and AP5.)