## 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)
- 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 | 10.11.2023 at 14:00h | Room 528, Building E1 3 |

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

Student-topic assignment announced | by 15.11.2023 | – on this website – |

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

Registration in LSF due | 6.12.2023 | – via LSF – |

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

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

Seminar presentations | w/c 5.2.2024 | 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: Lucas Kehrer
- 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: Fabian Brenner
- Presentation:
**—**

## Quantitative Strongest Postcondition **(BA)**

*Zhang & Kaminski.*Quantitative Strongest Post- Student: Christopher Cohnen
- 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: Clara Rubeck
- Presentation: —

### Algebraic Reasoning

## Refinement Algebra

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