Wednesday, September 2, 2015
11:30am Meeting room 302 (Mountain View), level 3
Joost-Pieter Katoen, Full Professor, RWTH Aachen, Germany
Understanding and Analyzing Probabilistic Programs
Abstract:
We present two semantic views of probabilistic programs and their relationship. An operational interpretation as well as a weakest precondition semantics are provided for an elementary probabilistic guarded command language. Our study treats features such as random sampling, conditioning, loop divergence, and non-determinism.
We then discuss two key analysis problems: almost-sure termination (does a program terminate with probability one?) and loop invariant synthesis.