Seminar
SS 2023
| 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)
- 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!
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 | 16.5.2023 at 14:15 | Room 528, Building E1 3 |
| Bidding for topics | 17.5.2023 | |
| Student-topic assignment announced | 19.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 due | 29.6.2023 | – via email – |
| Preliminary slides due (optional) | 13.7.2023 | – via email – |
| Seminar presentations | w/c 21.8.2023 | 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: —
Expected Runtimes (BA)
- Kaminski et al. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
- Student: —
- Presentation: —
Relative Completeness (BA)
- Batz et al. Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-based Reasoning
- Student: —
- Presentation: —
Reasoning with Probability Generating Functions (BA)
- Klinkenberg et al. Generating Functions for Probabilistic Programs
- Student: —
- Presentation: —
Correctness by Construction (BA)
- McIver & Morgan. Correctness by Construction for Probabilistic Programs
- Student: —
- Presentation: —
Relational Reasoning (BA)
- Aguirre et al. A Pre-Expectation Calculus for Probabilistic Sensitivity
- Student: —
- Presentation: —
Incorrectness Reasoning
Incorrectness Logic I (BA)
- de Vries & Koutavas. Reverse Hoare Logic
- Student: —
- Presentation: —
Incorrectness Logic (BA)
- O’Hearn. Incorrectness Logic
- Student: —
- Presentation: —
Quantitative Strongest Postcondition (BA)
- Zhang & Kaminski. Quantitative Strongest Post
- Student: —
- Presentation: —
Lower Bounds on Least Fixed Points
Lower Bounds on Expected Values
- Hark et al. Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
- Student: —
- Presentation: —
Lower Bounds on Least Fixed Points
- Baldan et al. Fixpoint Theory – Upside Down
- Student: —
- Presentation: —
Separation Logic
Separation Logic (BA)
- Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures [18]
- Student: —
- Presentation: —
Quantitative Separation Logic (BA)
- Batz et al. Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
- Student: —
- Presentation: —
Probabilistic Separation Logic
- Literature: Barthe, Hsu, & Liao. A Probabilistic Separation Logic
- Student: —
- Presentation: —
Separation Logic and Stochastic Independence I
- Bao et al. A Bunched Logic for Conditional Independence
- Student: —
- Presentation: —
Separation Logic and Stochastic Independence II
- Bao et al. A Separation Logic for Negative Dependence
- Student: —
- Presentation: —
Probabilistic Programming
Domain Theory for Statistical Probabilistic Programming
- Vákár, Kammar, & Staton. A Domain Theory for Statistical Probabilistic Programming
- Student: —
- Presentation: —
Reactive Programs
- Baudart et al. Reactive Probabilistic Programming
- Student: —
- Presentation: —
Neural Networks
Tropical Geometry of Neural Networks
- Zhang, Naitzat, & Lim. Tropical Geometry of Neural Networks
- Student: —
- Presentation: —