+**********************************************************************
*
*
*                          Einladung
*
*
*
*                     Informatik-Oberseminar
*
*
*
+**********************************************************************

Zeit:  Freitag, 18. Juni 2021, 15.00 Uhr

Ort: Zoom-Videokonferenz

Link:  https://rwth.zoom.us/j/94806153993?pwd=dUIwQWYxNUx1cG1jOEpLc25WdmJwUT09

Referent: Marcel Hark M.Sc.
          Lehr- und Forschungsgebiet Informatik 2

Thema: Towards Complete Methods for Automatic Complexity and Termination Analysis of (Probabilistic) Programs

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 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.

Es laden ein: die Dozentinnen und Dozenten der Informatik