Seminar Deductive Verification

Seminar in Theoretical CS, Winter 2023/24


  • 05.06.2023: We are online!

Introduction and Assignment of Topics

  • Slides of introduction (TBA)

Dates & Deadlines

Oct 11, 2023; 16:30Kick-off meeting (CS Department, building E1, 2nd floor, room 4201b)
TBATopic preferences due
TBADetailed outline due
TBAFull report due
TBAPresentation slides due
TBASeminar talks

Note that the full versions of your report and your slides should be your final submission and the camera-ready versions should differ only with regard to minor remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting preliminary versions before the due dates.


How can we make sure that programs behave correctly according to our specifications? Deductive Program Verification uses deductive reasoning to prove that programs satisfy certain specifications. Specifications may be a pair of pre- and post-conditions for a program (“if the input satisfies…, then the output satisfies…”), or may be more complex (e.g. hyperproperties). This line of research was very successful and resulted in nice-to-use verifiers like Microsoft’s Dafny. In this seminar, we’ll look into current research related to deductive program verification with goals of making program verification easier to use, reason about more properties, and enable more automation.


Basic knowledge in Formal Languages and Automata Theory and Mathematical Logic is expected. For some of the topics, experience with Formal Semantics of Programming Languages and Probabilistic Programming is helpful.


Note: There may be some changes to the final list of topics.

Deductive Verification in Practice
1Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers:
The Prusti Project: Formal Verification for Rust. NFM 2022
2Franck Cassez, Joanne Fuller, Horacio Mijail Anton Quiles:
Deductive Verification of Smart Contracts with Dafny. FMICS 2022
3Gaurav Parthasarathy, Peter Müller, Alexander J. Summers:
Formally Validating a Practical Verification Condition Generator. CAV 2021
4Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha:
egg: Fast and extensible equality saturation. POPL 2021
Verification Languages
5K. Rustan M. Leino:
Automating Induction with an SMT Solver. VMCAI 2012
6K. Rustan M. Leino, Nadia Polikarpova:
Verified Calculations. VSTTE 2013
7Petra van den Bos, Sung-Shik Jongmans:
VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. FM 2023
8JC Filliâtre: One Logic to Use Them All. CADE 2013
Probabilistic Programs
9Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács:
This is the moment for probabilistic loops. OOPSLA 2022
10Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan:
Lower Bounds for Possibly Divergent Probabilistic Programs. OOPSLA 2023
11Linpeng Zhang, Benjamin Lucien Kaminski:
Quantitative strongest post: a calculus for reasoning about the flow of quantitative information. OOPSLA 2022
12Fabian Zaiser, Andrzej S Murawski, Luke Ong: Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach. arXiv Preprint 2023


Registration to the seminar is handled via the SuPra system.

Grading Scheme

You can access the grading scheme here:

Additional Material


Philipp Schroer