+********************************************************************** * * * 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 -- Marcel Hark Research Group Computer Science 2 RWTH Aachen University Ahornstr. 55 52074 Aachen Germany E-Mail: marcel.hark@cs.rwth-aachen.de" Phone: +49-241/80-21218 Fax: +49-241/80-22217 Room: 4208