Aspects of Quantitative Program Verification (SS 2023)


SS 2023

OrganizersProf. Benjamin Kaminski, Lena Verscht, Tobias Gürtler

Are you passionate about logic, verification, semantics, and alike? Are you tired of thinking black-and-white, true-or-false? Then come and study the more nuanced quantitative formal program verification! In quantitative verification, properties are not just true or false. Instead, we verify quantities like runtimes, error probabilities, beliefs, etc.

Topics which we will cover include:

  • Probabilistic programming (a currently trending modeling paradigm in machine learning)
  • The geometry of neural networks
  • Incorrectness logic (the latest creation of the former chief formal methods researcher at Facebook)
  • Quantitative Information Flow
  • Worst-case (expected) execution times
  • Verification of heap-manipulating programs
  • and many more…

Find the full list of topics that we will cover below!


MandatoryProgrammierung 1
Programmierung 2
Grundzüge der Theoretischen Informatik
Introduction to Computational Logic
Automata, Games and Verification


The report must be prepared using the ACM template acmart-pacmpl-template.tex with the following options in the preamble:


The report must not exceed 10 pages, excluding references.


As a block seminar at the end of the semester.

More information TBA.

Timeline / Deadlines (tentative)

Kick-off meeting16.5.2023 at 14:15Room 528, Building E1 3
Bidding for topics17.5.2023
Student-topic assignment announced19.5.2023– on this website –
Last chance to
withdraw from seminar
9.6.2023– in LSF/HISPOS –
Detailed report outline +
1 page of main part due
7.6.2023– via email –
Final report due29.6.2023– via email –
Preliminary slides due (optional)13.7.2023– via email –
Seminar presentationsw/c 21.8.2023Room 528, Building E1 3
w/c = week commencing


Topics marked (BA) are particularly well-suited for Bachelor students.

Generalized Hoare Logics & Predicate Transformers

Weighted Programming

Expected Runtimes (BA)

Reasoning with Probability Generating Functions (BA)

Correctness by Construction (BA)

Relational Reasoning (BA)

Incorrectness Reasoning

Incorrectness Logic I (BA)

Incorrectness Logic (BA)

Quantitative Strongest Postcondition (BA)

Lower Bounds on Least Fixed Points

Lower Bounds on Expected Values

Lower Bounds on Least Fixed Points

Separation Logic

Separation Logic (BA)

Quantitative Separation Logic (BA)

Probabilistic Separation Logic

Separation Logic and Stochastic Independence I

Separation Logic and Stochastic Independence II

Probabilistic Programming

Domain Theory for Statistical Probabilistic Programming

Reactive Programs

Neural Networks

Tropical Geometry of Neural Networks