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 | 11.11.2024 at 14: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: —
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: —
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: —
Outcome Logic
- Zilberstein et al. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness
- Student: —
- Presentation: —
Differential Privacy
- Barthe et al. Proving differential privacy in Hoare logic
- 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: —
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: —
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
- Bao et al. A Bunched Logic for Conditional Independence
- 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: —
Reactive Programs
- Baudart et al. Reactive 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: —
Verifying Neural Networks
Reachable Specifications (BA)
- Singh et al. An Abstract Domain for Certifying Neural Networks
- Student: —
- Presentation: —
Residual Reasoning (BA)
- Elboher et al. On applying residual reasoning within neural network verification
- Student: —
- Presentation: —