## Seminar

SS 2022

Organizer | Prof. Benjamin Kaminski |

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 |

Recommended | Grundzüge der Theoretischen Informatik |

Nice-to-have | 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 | Monday, April 25, 14:30 – 16:00 | Seminar room 0.16, Building E1 3 |

Bidding for topics | Wednesday, April 27 | |

Student-topic assignment announced | by Friday, April 29 | – on this website – |

Last chance to withdraw from seminar | Monday, May 16 | – in LSF/HISPOS – |

Detailed report outline + 1 page of main part due | Friday, May 27 | – via email – |

Final report due | Friday, July 1 | – via email – |

Preliminary slides due (optional) | Monday, July 18 | – via email – |

Seminar presentations | Monday, August 29, 14:30 – ca. 18:00 and Tuesday, August 30, 14:00 – ca. 18:00 | Room 528, Building E1 3 |

# Topics

Topics marked **(BA)** are particularly well-suited for Bachelor students.

## Generalized Hoare Logics & Predicate Transformers

## Belief Programming

*Atkinson & Carbin.*Programming and Reasoning with Partial Observability [1]- Student:
**—** - Presentation: —

## Weighted Programming

*Batz et al.*Weighted Programming – A Programming Paradigm for Specifying Mathematical Models [6]- Student:
**Yannik Schnitzer** - Presentation: Monday, August 29, 14:30

## Expected Runtimes **(BA)**

*Kaminski et al.*Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs [13]- Student:
**Mohamed Samrah** - Presentation: Monday, August 29, 15:15

## Relative Completeness **(BA)**

*Batz et al.*Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-based Reasoning [7]- Student: —
- Presentation: —

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

*Klinkenberg et al.*Generating Functions for Probabilistic Programs [14]- Student:
**Peter Gastauer** - Presentation: Monday, August 29, 17:15

## Correctness by Construction **(BA)**

*McIver & Morgan.*Correctness by Construction for Probabilistic Programs [16]- Student:
**Omar Al Jbawi** - Presentation: Monday, August 29, 16:30

## Incorrectness Reasoning

## Incorrectness Logic **(BA)**

*O’Hearn.*Incorrectness Logic [17]- Student:
**Jonas Schäfer** - Presentation: Tuesday, August 30, 14:45

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

*Zhang & Kaminski.*Quantitative Strongest Post [20]- Student: —
- Presentation: TBA

### 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 [10]- Student: —
- Presentation: —

## Lower Bounds on Least Fixed Points

*Baldan et al.*Fixpoint Theory – Upside Down [2]- Student: —
- Presentation: —

### Separation Logic

## Separation Logic **(BA)**

*Reynolds*. Separation Logic: A Logic for Shared Mutable Data Structures [18]- Student: —
- Presentation: TBA

## Quantitative Separation Logic **(BA)**

*Batz et al.*Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs [8]- Student:
**Haoyi Zeng** - Presentation: Tuesday, August 30, 14:00

## Probabilistic Separation Logic

- Literature:
*Barthe, Hsu, & Liao.*A Probabilistic Separation Logic [5] - Student: —
- Presentation: —

## Separation Logic and Stochastic Independence I

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

## Separation Logic and Stochastic Independence II

*Bao et al.*A Separation Logic for Negative Dependence [4]- Student: —
- Presentation: —

### Probabilistic Programming

## Verified Variational Inference

*Lee et al.*Towards Verified Stochastic Variational Inference for Probabilistic Programs [15]- Student: —
- Presentation: —

## Domain Theory for Statistical Probabilistic Programming

*Vákár, Kammar, & Staton.*A Domain Theory for Statistical Probabilistic Programming [19]- Student: —
- Presentation: —

### Conditioning in Probabilistic Programming

## Conditioning I (Paradoxes)

*Jules Jacobs.*Paradoxes of Probabilistic Programming: And How To Condition on Events of Measure Zero with Infinitesimal Probabilities [12]- Student:
**Koushik Chowdhury** - Presentation: Tuesday, August 30, 17:15

## Conditioning II (Conditioning within Loops)

*Baudart et al.*Reactive Probabilistic Programming [9]- Student: —
- Presentation: —

## Conditioning III (Update Rules)

*Jacobs.*The Mathematics of Changing One’s Mind, via Jeffrey’s or Pearl’s Update Rule [11]- Student:
**Tobias Gürtler** - Presentation: Tuesday, August 30, 16:30

### Neural Networks

## Tropical Geometry of Neural Networks

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

### Literature

- [1]Eric Atkinson and Michael Carbin. 2020. Programming and reasoning with partial observability.
*Proceedings of the ACM on Programming Languages*, 1–28. DOI:https://doi.org/10.1145/3428268 - [2]Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. 2021. Fixpoint Theory – Upside Down.
*Lecture Notes in Computer Science*, 62–81. DOI:https://doi.org/10.1007/978-3-030-71995-1_4 - [3]Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. 2021. A Bunched Logic for Conditional Independence.
*2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. DOI:https://doi.org/10.1109/lics52264.2021.9470712 - [4]Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti. 2022. A separation logic for negative dependence.
*Proceedings of the ACM on Programming Languages*, 1–29. DOI:https://doi.org/10.1145/3498719 - [5]Gilles Barthe, Justin Hsu, and Kevin Liao. 2020. A probabilistic separation logic.
*Proceedings of the ACM on Programming Languages*, 1–30. DOI:https://doi.org/10.1145/3371123 - [6]Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. 2022. Weighted Programming – A Programming Paradigm for Specifying Mathematical Models. Auckland, New Zeeland.
- [7]Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning.
*Proceedings of the ACM on Programming Languages*, 1–30. DOI:https://doi.org/10.1145/3434320 - [8]Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs.
*Proceedings of the ACM on Programming Languages*, 1–29. DOI:https://doi.org/10.1145/3290347 - [9]Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. 2020. Reactive probabilistic programming.
*Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation*. DOI:https://doi.org/10.1145/3385412.3386009 - [10]Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen. 2020. Aiming low is harder: induction for lower bounds in probabilistic program verification.
*Proceedings of the ACM on Programming Languages*, 1–28. DOI:https://doi.org/10.1145/3371105 - [11]Bart Jacobs. 2019. The Mathematics of Changing One’s Mind, via Jeffrey’s or via Pearl’s Update Rule.
*Journal of Artificial Intelligence Research*, 783–806. DOI:https://doi.org/10.1613/jair.1.11349 - [12]Jules Jacobs. 2021. Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities.
*Proceedings of the ACM on Programming Languages*, 1–26. DOI:https://doi.org/10.1145/3434339 - [13]Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo (Eds.). 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms.
*Journal of the ACM*, 1–68. DOI:https://doi.org/10.1145/3208102 - [14]Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, and Tobias Winkler. 2021. Generating Functions for Probabilistic Programs.
*Logic-Based Program Synthesis and Transformation*, 231–248. DOI:https://doi.org/10.1007/978-3-030-68446-4_12 - [15]Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. 2020. Towards verified stochastic variational inference for probabilistic programs.
*Proceedings of the ACM on Programming Languages*, 1–33. DOI:https://doi.org/10.1145/3371084 - [16]Annabelle McIver and Carroll Morgan. 2020. Correctness by Construction for Probabilistic Programs.
*Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles*, 216–239. DOI:https://doi.org/10.1007/978-3-030-61362-4_12 - [17]Peter W. O’Hearn. 2020. Incorrectness logic.
*Proceedings of the ACM on Programming Languages*, 1–32. DOI:https://doi.org/10.1145/3371078 - [18]J.C. Reynolds. Separation logic: a logic for shared mutable data structures.
*Proceedings 17th Annual IEEE Symposium on Logic in Computer Science*. DOI:https://doi.org/10.1109/lics.2002.1029817 - [19]Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming.
*Proceedings of the ACM on Programming Languages*, 1–29. DOI:https://doi.org/10.1145/3290349 - [20]Linpeng Zhang and Benjamin Lucien Kaminski. 2022. Quantitative Strongest Post – A Calculus for Reasoning about the Flow of Quantitative Information. Auckland, New Zeeland.
- [21]Liwen Zhang, Gregory Naitzat, and Lek-Heng Lim. 2018. Tropical Geometry of Deep Neural Networks. In
*ICML*, PMLR, 5819–5827.