## Seminar

SS 2023

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 | 16.5.2023 at 14:15 | Room 528, Building E1 3 |

Bidding for topics | 17.5.2023 | |

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

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

Detailed report outline + 1 page of main part due | 7.6.2023 | – via email – |

Final report due | 29.6.2023 | – via email – |

Preliminary slides due (optional) | 13.7.2023 | – via email – |

Seminar presentations | w/c 21.8.2023 | 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: —

## Reasoning with Probability Generating Functions **(BA)**

*Klinkenberg et al.*Generating Functions for Probabilistic Programs- 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:
**—**

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

### Lower Bounds on Least Fixed Points

## Lower Bounds on Expected Values

*Hark et al.*Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification- Student: —
- Presentation: —

## Lower Bounds on Least Fixed Points

*Baldan et al.*Fixpoint Theory – Upside Down- 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 I

*Bao et al.*A Bunched Logic for Conditional Independence- Student: —
- Presentation: —

## Separation Logic and Stochastic Independence II

*Bao et al.*A Separation Logic for Negative Dependence- 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: —

### Neural Networks

## Tropical Geometry of Neural Networks

*Zhang, Naitzat, & Lim.*Tropical Geometry of Neural Networks- Student: —
- Presentation: —