Joost-Pieter Katoen is a distinguished professor at RWTH
Aachen University in the Software Modeling and Verification (MOVES)
group and is part-time associated to the Formal Methods & Tools Group at
the University of Twente (NL). He is interested in model checking,
concurrency theory, program analysis and formal semantics. He is a
member of the Academia Europaea, received an honorary doctorate from
Aalborg University, is ERC Advanced Grant holder and was recently named
ACM Fellow.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Kaiserslautern

Program termination is a key question in program verification. This talk considers the termination of probabilistic programs, programs that can describe e.g., randomized algorithms, security algorithms and Bayesian learning.

Probabilistic termination has several nuances. Diverging program runs may occur with probability zero. Such programs are almost surely terminating (AST). If the expected duration until termination is finite, they are positive AST.

This talk presents a simple though powerful proof rule for deciding AST, reports on recent approaches towards automation, and sketches a Dijkstra-like weakest precondition calculus for proving positive AST in a compositional way.

-------------

Please contact MPI-SWS Office Team for Zoom link information

Susanne Girard

+49 631 9303 9605

--email hidden

public