199.100 Verification of Probabilistic Programs
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2022S, VU, 2.0h, 3.0EC, wird geblockt abgehalten

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Präsenz

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

After successful completion of the course, students will

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

Inhalt der Lehrveranstaltung

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)

 

Methoden

Lecturing with exercises.


Prüfungsmodus

Schriftlich

Weitere Informationen

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.

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
16:00 - 18:0002.05.2022 - 13.05.2022Seminarraum DE0110 Verification of Probabilistic Programs
Fr.14:00 - 16:0013.05.2022Seminarraum DE0110 Verification of Probabilistic Programs
Verification of Probabilistic Programs - Einzeltermine
TagDatumZeitOrtBeschreibung
Mo.02.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Di.03.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Mi.04.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Do.05.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Fr.06.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Mo.09.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Di.10.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Mi.11.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Do.12.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
Fr.13.05.202214:00 - 16:00Seminarraum DE0110 Verification of Probabilistic Programs
Fr.13.05.202216:00 - 18:00Seminarraum DE0110 Verification of Probabilistic Programs
LVA wird geblockt abgehalten

Leistungsnachweis

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

LVA-Anmeldung

Von Bis Abmeldung bis
11.02.2022 00:00 02.05.2022 23:59

Anmeldemodalitäten

Please register in TISS.

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Probability theory. Programming languages. Logic.

Weitere Informationen

  • Anwesenheitspflicht!

Sprache

Englisch