25^th Estonian Winter School in Computer Science (EWSCS)
XXV Eesti Arvutiteaduse Talvekool

Joost-Pieter Katoen

Software Modeling and Verification (MOVES) group
RWTH Aachen
Germany

Formal Methods & Tools group
Universiteit Twente
The Netherlands

Foundations of probabilistic programming

Abstract

Probabilistic programming combines probability theory, statistics and programming languages. They allow to model a much larger class of models in a rather succinct manner. The full potential of modern probabilistic programming languages comes from automating the process of inferring unobserved variables in the model conditioned on observed data. As some researchers put it: "The goal of probabilistic programming is to enable probabilistic modeling and machine learning to be accessible to the working programmer."

Probabilistic programs steer autonomous robots, are at the heart of security mechanisms, encompass randomised algorithms, and are used in AI to infer statistical conclusions about huge amounts of uncertain data.

In these lectures, I will introduce the main underlying concepts of probabilistic programming, and discuss how classical program verification à la Dijkstra can be used to answer elementary questions such as: Do these programs terminate at all? With what probability? How many resources do they consume?, etc. Applications to Bayesian networks will show how insightful information about analysing such networks can be obtained in a fully automated manner by using program verification.

Course materials

• J.-P. Katoen. Foundations of probabilistic programming. Slides from EWSCS 2020.
  • Lecture 1 [pdf]
  • Lecture 2 [pdf]
  • Lecture 3 [pdf]
  • Lecture 4 [pdf]
• J.-P. Katoen. Exercise class problems from EWSCS 2020, with solutions. [pdf, password-protected]


• Videos from the lectures (large, unedited files) [mp4, password-protected]


• B. Kaminski, J.-P. Katoen, C. Matheja. Expected runtime analysis by program verification. In Foundations of Probabilistic Programming, Cambridge Univ. Press, to appear. Draft version [pdf, password-protected]
• A. McIver, C. Morgan, B. Kaminski, J.-P. Katoen. A new proof rule for almost-sure termination. Proc. ACM Program. Lang., v. 2, n. POPL, article 33, 2018. [doi]
• F. Gretz, J.-P. Katoen, A. McIver. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Evaluation, v. 73, pp. 110-132, 2014. [doi]
• F. Olmedo, F. Gretz, N. Jansen, B. Kaminski, J.-P. Katoen, A. McIver. Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst., v. 40, n. 1, article 4, 2018. [doi]

Last changed April 10, 2020 22:30 Europe/Helsinki (GMT +03:00) by local organizers, ewscs20(at)cs.ioc.ee
EWSCS'20 page: //cs.ioc.ee/ewscs/2020/