## Seminar

WS 2023/2024

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

Bidding for topics | TBA | |

Student-topic assignment announced | TBA | – on this website – |

Last chance to withdraw from seminar | TBA | – in LSF/HISPOS – |

Detailed report outline + 1 page of main part due | TBA | – via email to your supervisor – |

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

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

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

## 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

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

### Algebraic Reasoning

## Refinement Algebra

*von Wright*. Towards a refinement algebra- Student: —
- Presentation: —