Friday September 26, Friedrich Gretz successfully defended his PhD dissertation, entitled “Semantics and Loop Invariant Synthesis for Probabilistic Programs” for a jury consisting of Sriram Sankaranarayanan (Boulder, USA), Stefan Kowalewski, Jürgen Giesl, and Joost-Pieter Katoen (all Aachen).  Friedrich’s dissertation studies weakest pre-condition semantics, relates this to operational semantics, and extends this to including observations.  In addition, he developed the Prinsys tool for constraint-based loop invariant inference for probabilistic programs.