Organizers	Prof. Benjamin Kaminski, Lena Verscht, Tobias Gürtler
Places	12

---

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)
• 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!

Prerequisites

Mandatory	Programmierung 1 Programmierung 2 Grundzüge der Theoretischen Informatik
Recommended	Semantics Introduction to Computational Logic Automata, Games and Verification
Ideal	Verification

Reports

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

\documentclass[acmsmall,dvipsnames,x11names,svgnames,cleveref]{acmart}
\settopmatter{printfolios=true,printccs=false,printacmref=false}

The report must not exceed 10 pages, excluding references.

Presentations

As a block seminar at the end of the semester.

More information TBA.

Timeline / Deadlines (tentative)

Kick-off meeting	10.11.2023 at 14:00h	Room 528, Building E1 3
Bidding for topics	13.11.2023	– via email to Benjamin Kaminski –
Student-topic assignment announced	by 15.11.2023	– on this website –
Detailed report outline + 1 page of main part due	30.11.2023	– via email to your supervisor –
Registration in LSF due	6.12.2023	– via LSF –
Final report due	22.12.2023	– via email to your supervisor –
Preliminary slides due (optional)	8.1.2024	– via email to your supervisor –
Seminar presentations	7.2.2024 at 14:00h	Room 528, Building E1 3

Topics

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

Generalized Hoare Logics & Predicate Transformers

Incorrectness Reasoning

Separation Logic

Probabilistic Programming

Algebraic Reasoning