Quantitative Verification Group

Aspects of Quantitative Program Verification (SS 2024)

Seminar

SS 2024

OrganizersProf. Benjamin Kaminski, Tobias Gürtler, Anran Wang
Places12
Kick-off meeting slides (from last semester)Download

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, nonacm]{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
6.5.2024 at 14:15
likely Room 528,
Building E1 3
Bidding for topics8.5.2024 – via email to Benjamin Kaminski –
Student-topic assignment announcedby 10.5.2024– on this website –
Detailed report outline +
1 page of main part due		23.5.2024– via email to your supervisor –
Registration in LSF dueTBA– via LSF –
Final report due20.6.2024– via email to your supervisor –
Preliminary slides due (optional)4.7.2024– via email to your supervisor –
Seminar presentationsw/c 22.7.2024 likely 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)

Relative Completeness (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

Exact Inference for Discrete Probabilistic Programs (BA)

Domain Theory for Statistical Probabilistic Programming

Reactive Programs

Algebraic Reasoning

Refinement Algebra