Towards complete methods for automatic complexity and termination analysis of (probabilistic) programs

• Methoden für die automatische Komplexitäts- und Terminierungsanalyse von (probabilistischen) Programmen und ihre Vollständigkeit

Hark, Marcel Tobias; Giesl, Jürgen (Thesis advisor); Kovács, Laura (Thesis advisor)

Aachen : RWTH Aachen University (2021)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2021

Abstract

The increasing importance of computer programs in our everyday life has led to more and more complex software systems. To prove correctness of such a system, formal verification is the standard methodology. Two of the most important properties of a program are its termination behavior and its efficiency. Moreover, in recent years randomization in programming has gained a lot of interest. For example, to model non-deterministic behavior in real-world applications, probabilistic concepts have proved very successful. In this thesis, we investigate formal verification of programs which also feature assignments via discrete probability distributions. In particular, we are interested in proving (non-)termination and inferring bounds on the (expected) worst-case runtime of such programs. In general, formal verification of programs is undecidable. Still, whenever possible, complete approaches for verifying certain properties on (sub-)classes of programs are preferable to incomplete ones since they always yield definite results, i.e., either a proof or a counterexample. Hence, we characterize sub-classes of programs for which we can present complete approaches for analyzing termination and runtime complexity. To analyze systems arising from real-world applications, formal verification has to proceed automatically. Thus, we also investigate the automation of our results.The contributions of this thesis are as follows: (1) We characterize classes of non-probabilistic programs where both termination on a single input as well as all inputs are decidable, witnesses for non-termination are recursively enumerable, and upper bounds on the runtime can always be computed. (2) We connect the semantics of probabilistic programs that is defined via so-called expectation transformers to the semantics defined via so-called stochastic processes.This leads to the first inductive proof rules for lower bounds on expected outcomes and expected runtimes of probabilistic programs. (3) We present a class of probabilistic programs where not only probabilistic termination is decidable and both upper and lower bounds on the expected runtime can easily be inferred but also a closed form for the exact expected runtime can always be computed. (4) We develop an approach for deriving upper bounds on the expected runtime of general probabilistic programs. To this end, we use non-probabilistic runtime and size bounds as well as an alternating computation of expected runtime and size bounds. Our experiments demonstrate the performance and the applicability of this approach.

Institutions

• UnRAVeL Research Training Group [080060]
• Department of Computer Science [120000]
• Research Group Computer Science (Programming Languages and Verification) [121420]