Graduate Seminar: Marcel Hark: Towards Complete Methods for Automatic Complexity and Termination Analysis of (Probabilistic) Programs

Friday, June 18, 2021, 3:00pm

Location: Online session (Zoom Meeting)

Speaker: Marcel Hark



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 talk, 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 also 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 discuss the automation of our results as well.