Seminar Deductive Verification

Seminar in Theoretical CS, Winter 2023/24

News

  • 05.06.2023: We are online!
  • 19.10.2023: Assignment of topics online.
  • 26.10.2023: All supervisors have been assigned.

Introduction

Dates & Deadlines

Oct 11, 2023; 16:30Kick-off meeting (CS Department, building E1, 2nd floor, room 4201b)
Oct 16, 2023Topic preferences due
Nov 20, 2023Detailed outline due
Dec 18, 2023Full report due
Jan 15, 2024Presentation slides due
Jan 24, 2024Seminar 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

No.TopicStudentSupervisor
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		Emil Beothy-EloPhilipp Schroer
Verification Languages
5K. Rustan M. Leino:
Automating Induction with an SMT Solver. VMCAI 2012		Svenja SteinRaphael Berton
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		Jonas HartwigIra Fesefeldt
8JC Filliâtre: One Logic to Use Them All. CADE 2013Franz Leonard LinkPhilipp Schroer
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 2023Mohamed Majid Ben YahiaLutz Klinkenberg

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

Contact

Philipp Schroer