Organizers	Prof. Benjamin Kaminski, Tobias Gürtler, Anran Wang, Lucas Kehrer
Places	12

---

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

Prerequisites

Mandatory	TBA
Recommended	TBA
Ideal	TBA

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	TBA	likely Room 528, Building E1 3
Bidding for topics	TBA	– via email to Benjamin Kaminski –
Student-topic assignment announced	TBA	– on this website –
Detailed report outline + 1 page of main part due	TBA	– via email to your supervisor –
Registration in LSF due	TBA	– via LSF –
Final report due	TBA	– via email to your supervisor –
Preliminary slides due (optional)	TBA	– via email to your supervisor –
Seminar presentations	TBA	Room 528, Building E1 3

Topics

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

(Complete) Lattices

Antitone Functions (BA)

• Dacic. On Fixed Edges of Antitone Self-Mappings of Complete Lattices.
• Student: —
• Presentation: —

• Torres-ruiz et al. On Iteration in Discrete Probabilistic Programming
• Student: —
• Presentation: —

⁠Sound Fixed Point Iteration (BA)

• Quatmann and Katoen. Sound Value Iteration
• Student: —
• Presentation: —

Deriving Upper Points in Probabilistic Programs

• Batz et al. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
• Student: —
• Presentation: —

Latticed k-Induction

• Batz et al. Latticed k-Induction with an Application to Probabilistic Programs
• Student: —
• Presentation: —

Expressive Equivalence of Fixed Point Logics

• Kreutzer. Expressive equivalence of least and inflationary fixed-point logic
• Student: —
• Presentation: —

Model-guided Synthesis

• Murali et al. Model-guided synthesis of inductive lemmas for FOL with least fixpoints
• Student: —
• Presentation: —

Expected Rewards as Least Fixed Points (BA)

• Batz et al. J-P: MDP. FP. PP.
• Student: —
• Presentation: —

Guarded Fixed Point Logic

• Grädel and Walukiewicz. Guarded fixed point logic
• Student: —
• Presentation: —

Co-Induction

Latticed k-Induction

• Hur et al. The power of parameterization in coinductive proof
• Student: —
• Presentation: —

Coinductive Datastructurs

• Ralf Hinze. Functional Pearl: Streams and Unique Fixed Points
• Student: —
• Presentation: —

μ-Calculus

μ-Calculus and Category Theory

• Enqvist et al. Completeness for μ-Calculi: A Coalgebraic Approach.
• Student: —
• Presentation: —

Expressiveness of μ-Calculus (BA)

• Marti and Venema. Focus-Style Proof Systems and Interpolation for the Alternation-Free μ-Calculus.
• Student: —
• Presentation: —