Seminar in Theoretical CS, Winter 2023/24
News
- 05.06.2023: We are online!
Introduction and Assignment of Topics
- Slides of introduction (TBA)
Dates & Deadlines
| Oct 11, 2023; 16:30 | Kick-off meeting (CS Department, building E1, 2nd floor, room 4201b) |
| TBA | Topic preferences due |
| TBA | Detailed outline due |
| TBA | Full report due |
| TBA | Presentation slides due |
| TBA | Seminar 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.
Overview
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.
Prerequisites
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.
Topics
Note: There may be some changes to the final list of topics.
| No. | Topic | Student | Supervisor |
|---|---|---|---|
| Deductive Verification in Practice | |||
| 1 | Vytautas 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 | ||
| 2 | Franck Cassez, Joanne Fuller, Horacio Mijail Anton Quiles: Deductive Verification of Smart Contracts with Dafny. FMICS 2022 | ||
| 3 | Gaurav Parthasarathy, Peter Müller, Alexander J. Summers: Formally Validating a Practical Verification Condition Generator. CAV 2021 | ||
| 4 | Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha: egg: Fast and extensible equality saturation. POPL 2021 | ||
| Verification Languages | |||
| 5 | K. Rustan M. Leino: Automating Induction with an SMT Solver. VMCAI 2012 | ||
| 6 | K. Rustan M. Leino, Nadia Polikarpova: Verified Calculations. VSTTE 2013 | ||
| 7 | Petra van den Bos, Sung-Shik Jongmans: VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. FM 2023 | ||
| 8 | JC Filliâtre: One Logic to Use Them All. CADE 2013 | ||
| Probabilistic Programs | |||
| 9 | Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács: This is the moment for probabilistic loops. OOPSLA 2022 | ||
| 10 | Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan: Lower Bounds for Possibly Divergent Probabilistic Programs. OOPSLA 2023 | ||
| 11 | Linpeng Zhang, Benjamin Lucien Kaminski: Quantitative strongest post: a calculus for reasoning about the flow of quantitative information. OOPSLA 2022 | ||
| 12 | Fabian Zaiser, Andrzej S Murawski, Luke Ong: Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach. arXiv Preprint 2023 | ||
Registration
Registration to the seminar is handled via the SuPra system.
Grading Scheme
You can access the grading scheme here: https://moves.rwth-aachen.de/wp-content/uploads/seminar_grading_scheme.pdf
Additional Material
- Report template (TBA)
- Presentation template (TBA)
- How to Write a Seminar Paper
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
- How to Give Presentations
- Introduction to LaTeX