199.100 Verification of Probabilistic Programs
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2022S, VU, 2.0h, 3.0EC, to be held in blocked form

Properties

  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise
  • Format: Presence

Learning outcomes

After successful completion of the course, students are able to...

a.  have an acquaintenance with the core concepts of probabilistic programming:
sampling, conditioning, and querying.
b. be familiar with the probabilistic programming language WebPPL.
c. have a thorough understanding of the semantics of probabilistic programs.
d. know deductive verification techniques for proving elementary properties of probabilistic programs such as termination, expected outcomes, and expected runtimes.
e. have a basic understanding of the relationship with Bayesian networks.
f. have rudimentary knowledge on core verification topics such as loop invariants

Subject of course

The lecturer of this course will be Prof. Joost-Pieter Katoen / RWTH Aachen University (D) and University of Twente (NL).


Course abstract: Probabilistic programs feature sampling from probability distributions and the ability to condition values of variables in a program. The latter feature distinguishes modern probabilistic programming languages such as WebPPL, Pyro, Edward, Scenic, from those in the early days describing randomized algorithms.

Although probabilistic programs are normal–looking programs, reasoning about their correctness is intricate. They do not generate a single output but a distribution over outputs. Whereas a classical program terminates or not, this is no longer true for probabilistic programs.

They can diverge, but this may happen with probability zero. That is, even if programs terminate with probability one, they may have non-terminating runs.

 Establishing correctness of probabilistic programs needs—even more so than ordinary programs—formal reasoning. In this course, we will introduce probabilistic programs, their formal semantics, elementary decision problems and their complexity, and focus on the deductive verification of such programs.

Outline course content (subject to changes):

1. Introduction and WebPPL (2 hours)
2. pGCL: Syntax and Markov Semantics (2 hours)
3. Fixed Points and Dijkstra's Weakest Preconditions (2 hours)
4+5. Probabilistic Weakest Precondition Reasoning (4 hours)
6. Termination (2 hours)
7. Expected Runtime Analysis (2 hours)
8. Verifying Bayesian Networks (2 hours)
9. Probabilistic Separation Logic (2 hours)
10. Towards the Automated Verification of Probabilistic Programs (2 hours)



Teaching methods

Lecturing with exercises.

Mode of examination

Written

Additional information

This is a guest professor course of the TU Wien Informatics Doctoral School / Doctoral College "Resilient Embedded Systems".

The course is open to all PhD students and interested Master students.


Planned Course Schedule: May 2 - 13, 2022 and one week in June 2022.

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
16:00 - 18:0002.05.2022 - 13.05.2022Seminarraum DE0110 Verification of Probabilistic Programs
Fri14:00 - 16:0013.05.2022Seminarraum DE0110 Verification of Probabilistic Programs
Verification of Probabilistic Programs - Single appointments
DayDateTimeLocationDescription
Mon02.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Tue03.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Wed04.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Thu05.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Fri06.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Mon09.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Tue10.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Wed11.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Thu12.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Fri13.05.202214:00 - 16:00Seminarraum DE0110 Verification of Probabilistic Programs
Fri13.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Course is held blocked

Examination modalities

There will be a written exam at the end of the course.

Course registration

Begin End Deregistration end
11.02.2022 00:00 02.05.2022 23:59

Registration modalities

Please register in TISS.

Curricula

Literature

No lecture notes are available.

Previous knowledge

Probability theory. Programming languages. Logic.

Miscellaneous

  • Attendance Required!

Language

English