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

---

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	TBD TBD	Room 528, Building E1 3
Bidding for topics	until TBD	– via email to Benjamin Kaminski –
Student-topic assignment announced	by TBD	– on this website –
Detailed report outline + 1 page of main part due	TBD	– via email to your supervisor –
Registration in LSF due	TBD	– via LSF (your responsibility) –
Final report due	TBD	– via email to your supervisor –
Make an appointment for mandatory practice presentation with your supervisor	by TBD	– make appointment with your supervisor –
Seminar presentations	w/c TBD	likely 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

Parameterized Coinduction

• 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: —