## 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 | TBD | Likely Room 528, Building E1 3 |

Bidding for topics | TBD | – via email to Benjamin Kaminski – |

Student-topic assignment announced | 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 – |

Final report due | TBD | – via email to your supervisor – |

Preliminary slides due (optional) | TBD | – via email to your supervisor – |

Seminar presentations | TBD | 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: —