Seminar
WS 2024/2025
| Organizers | Prof. Benjamin Kaminski, Tobias Gürtler, Anran Wang |
| Places | 6 |
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/Meta)
- 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,nonacm]{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 | 12.11.2024 at 16:15 | Likely Room 528, Building E1 3 |
| Bidding for topics | 14.11.2024 | – via email to Benjamin Kaminski – |
| Student-topic assignment announced | by 15.11.2024 | – on this website – |
| Detailed report outline + 1 page of main part due | 26.11.2024 | – via email to your supervisor – |
| Registration in LSF due | TBD | – via LSF – |
| Final report due | 23.12.2024 | – via email to your supervisor – |
| Preliminary slides due (optional) | 7.1. | – via email to your supervisor – |
| Seminar presentations | w/c 20.1.2025 | Likely Room 528, Building E1 3 |
Topics
Topics marked (BA) are particularly well-suited for Bachelor students.
Generalized Hoare Logics & Predicate Transformers
Weighted Programming
- Batz et al. Weighted Programming – A Programming Paradigm for Specifying Mathematical Models
- Student: —
- Presentation: —
Outcome Logic
- Zilberstein et al. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness
- Student: —
- Presentation: —
General Correctness (BA)
- Jacobs & Gries General Correctness: A Unification of Partial and Total Correctness
- Student: —
- Presentation: —
General Correctness, Axiomatic
- Guttmann Partial, Total and General Correctness
- Student: —
- Presentation: —
Synthesis of Loop Invariants
- Batz et al. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
- Student: —
- Presentation: —
Resolving Nondeterminism (BA)
- Winkler et al. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
- Student: —
- Presentation: —
Probabilistic Programming
Scalable Inference (BA)
- Holtzen et al. Scaling Exact Inference for Discrete Probabilistic Programs
- Student: —
- Presentation: —
Domain Theory for Statistical Probabilistic Programming
- Vákár, Kammar, & Staton. A Domain Theory for Statistical Probabilistic Programming
- Student: —
- Presentation: —
Exact Symbolic Inference
- Gehr et al. PSI: Exact Symbolic Inference for Probabilistic Programs
- Student: —
- Presentation: —
Algebraic Reasoning
Refinement Algebra
- von Wright. Towards a refinement algebra
- Student: —
- Presentation: —
Fixed Points
Finding Fixed Points Syntactically (BA)
- Chuang & Goldberg. A syntactic method for finding least fixed points of higher-order functions over finite domains
- Student: —
- Presentation: —
Fixed Points and General Correctness
- Guttmann. Fixpoints for General Correctness
- Student: —
- Presentation: —
Calculating Loops (BA)
- Mili et al. Mathematics for reasoning about loop functions
- Student: —
- Presentation: —