Quantitative Verification Group

Aspects of Quantitative Program Verification (WS 22/23)

Seminar

WS 2022/2023

OrganizerProf. Benjamin Kaminski
Places12
Kick-off meeting slidesDownload

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)
  • The geometry of neural networks
  • 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 meeting14.11.2022
11:30		Room 528, Building E1 3
Bidding for topics16.11.2022
Student-topic assignment announcedby 18.11.2022– on this website –
Last chance to
withdraw from seminar		9.12.2022– in LSF/HISPOS –
Detailed report outline +
1 page of main part due		21.12.2022– via email –
Final report due25.1.2023– via email –
Preliminary slides due (optional)22.2.2023– via email –
Seminar presentations16.3.2023Room 528, Building E1 3
w/c = week commencing

Topics

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

Generalized Hoare Logics & Predicate Transformers

Belief Programming

Weighted Programming

Expected Runtimes (BA)

Relative Completeness (BA)

Reasoning with Probability Generating Functions (BA)

Correctness by Construction (BA)

Incorrectness Reasoning

Incorrectness Logic (BA)

  • O’Hearn. Incorrectness Logic ​[17]​
  • Student: Yasmine Briefs
  • Presentation: 16.3.2023, 11:00

Quantitative Strongest Postcondition (BA)

Lower Bounds on Least Fixed Points

Lower Bounds on Expected Values

Lower Bounds on Least Fixed Points

Separation Logic

Separation Logic (BA)

Quantitative Separation Logic (BA)

Probabilistic Separation Logic

Separation Logic and Stochastic Independence I

Separation Logic and Stochastic Independence II

Probabilistic Programming

Verified Variational Inference

Domain Theory for Statistical Probabilistic Programming

Conditioning in Probabilistic Programming

Conditioning I (Paradoxes)

Conditioning II (Conditioning within Loops)

Conditioning III (Update Rules)

Neural Networks

Tropical Geometry of Neural Networks

Literature

  1. [1]
    Eric Atkinson and Michael Carbin. 2020. Programming and reasoning with partial observability. Proceedings of the ACM on Programming Languages, 1–28. DOI:https://doi.org/10.1145/3428268
  2. [2]
    Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. 2021. Fixpoint Theory – Upside Down. Lecture Notes in Computer Science, 62–81. DOI:https://doi.org/10.1007/978-3-030-71995-1_4
  3. [3]
    Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. 2021. A Bunched Logic for Conditional Independence. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI:https://doi.org/10.1109/lics52264.2021.9470712
  4. [4]
    Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti. 2022. A separation logic for negative dependence. Proceedings of the ACM on Programming Languages, 1–29. DOI:https://doi.org/10.1145/3498719
  5. [5]
    Gilles Barthe, Justin Hsu, and Kevin Liao. 2020. A probabilistic separation logic. Proceedings of the ACM on Programming Languages, 1–30. DOI:https://doi.org/10.1145/3371123
  6. [6]
    Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. 2022. Weighted Programming – A Programming Paradigm for Specifying Mathematical Models. Auckland, New Zeeland.
  7. [7]
    Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proceedings of the ACM on Programming Languages, 1–30. DOI:https://doi.org/10.1145/3434320
  8. [8]
    Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proceedings of the ACM on Programming Languages, 1–29. DOI:https://doi.org/10.1145/3290347
  9. [9]
    Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. 2020. Reactive probabilistic programming. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. DOI:https://doi.org/10.1145/3385412.3386009
  10. [10]
    Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen. 2020. Aiming low is harder: induction for lower bounds in probabilistic program verification. Proceedings of the ACM on Programming Languages, 1–28. DOI:https://doi.org/10.1145/3371105
  11. [11]
    Bart Jacobs. 2019. The Mathematics of Changing One’s Mind, via Jeffrey’s or via Pearl’s Update Rule. Journal of Artificial Intelligence Research, 783–806. DOI:https://doi.org/10.1613/jair.1.11349
  12. [12]
    Jules Jacobs. 2021. Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities. Proceedings of the ACM on Programming Languages, 1–26. DOI:https://doi.org/10.1145/3434339
  13. [13]
    Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo (Eds.). 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM, 1–68. DOI:https://doi.org/10.1145/3208102
  14. [14]
    Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, and Tobias Winkler. 2021. Generating Functions for Probabilistic Programs. Logic-Based Program Synthesis and Transformation, 231–248. DOI:https://doi.org/10.1007/978-3-030-68446-4_12
  15. [15]
    Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. 2020. Towards verified stochastic variational inference for probabilistic programs. Proceedings of the ACM on Programming Languages, 1–33. DOI:https://doi.org/10.1145/3371084
  16. [16]
    Annabelle McIver and Carroll Morgan. 2020. Correctness by Construction for Probabilistic Programs. Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 216–239. DOI:https://doi.org/10.1007/978-3-030-61362-4_12
  17. [17]
    Peter W. O’Hearn. 2020. Incorrectness logic. Proceedings of the ACM on Programming Languages, 1–32. DOI:https://doi.org/10.1145/3371078
  18. [18]
    J.C. Reynolds. Separation logic: a logic for shared mutable data structures. Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. DOI:https://doi.org/10.1109/lics.2002.1029817
  19. [19]
    Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages, 1–29. DOI:https://doi.org/10.1145/3290349
  20. [20]
    Linpeng Zhang and Benjamin Lucien Kaminski. 2022. Quantitative Strongest Post – A Calculus for Reasoning about the Flow of Quantitative Information. Auckland, New Zeeland.
  21. [21]
    Liwen Zhang, Gregory Naitzat, and Lek-Heng Lim. 2018. Tropical Geometry of Deep Neural Networks. In ICML, PMLR, 5819–5827.