Joost-Pieter Katoen

"On Probabilistic Program Termination"

( MPI-SWS talk in Kooperation mit dem Fachbereich Informatik)

Program termination is a key question in program verification.This talk considers the termination of probabilistic programs, programsthat can describe e.g., randomized algorithms, security algorithms andBayesian learning.
Probabilistic termination has several nuances. Diverging program runsmay occur with probability zero. Such programs are almost surelyterminating (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 aDijkstra-like weakest precondition calculus for proving positive AST ina compositional way.

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

Termin als Datei downloaden und in den Kalender importieren.