Aspects of Quantitative Program Verification (WS 23/24)

Seminar

WS 2023/2024

OrganizersProf. Benjamin Kaminski, Lena Verscht, Tobias Gürtler
Places12

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)
  • 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

MandatoryProgrammierung 1
Programmierung 2
Grundzüge der Theoretischen Informatik
RecommendedSemantics
Introduction to Computational Logic
Automata, Games and Verification
IdealVerification

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
10.11.2023 at 14:00h
Room 528,
Building E1 3
Bidding for topics13.11.2023 – via email to Benjamin Kaminski –
Student-topic assignment announcedby 15.11.2023– on this website –
Detailed report outline +
1 page of main part due
30.11.2023– via email to your supervisor –
Registration in LSF due6.12.2023– via LSF –
Final report due22.12.2023– via email to your supervisor –
Preliminary slides due (optional)8.1.2024– via email to your supervisor –
Seminar presentations7.2.2024 at 14:00h Room 528, Building E1 3
w/c = week commencing

Topics

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

Generalized Hoare Logics & Predicate Transformers

Weighted Programming

Expected Runtimes (BA)

Correctness by Construction (BA)

Relational Reasoning (BA)

Outcome Logic

Differential Privacy

Incorrectness Reasoning

Incorrectness Logic I (BA)

Incorrectness Logic (BA)

Quantitative Strongest Postcondition (BA)

Separation Logic

Separation Logic (BA)

Quantitative Separation Logic (BA)

Probabilistic Separation Logic

Separation Logic and Stochastic Independence

Probabilistic Programming

Domain Theory for Statistical Probabilistic Programming

Reactive Programs

Algebraic Reasoning

Refinement Algebra