Overview

About

When designing programs/algorithms for quantum computers, one would like to know for sure what they do / whether they are correct. Like in the case of classical programs, it is possible to reason about programs using “program logics”. Examples of such logics (that you might know of from earlier courses) are Hoare logics, weakest precondition transformers, type systems, etc. Another approach to verify programs is to use model checking (i.e. translate the program into e.g. a Markov Chain first, and then check properties of it).

In this seminar, the participant will be studying such program logics / topics from quantum model checking from a scientific paper, and present the results to their peers in a talk and a seminar report.

Prerequisites

You should have taken an introductory course related to quantum computing or quantum algorithms. (E.g., Introduction to Quantum Computing) It is beneficial if you have already studied logics in the classical (or even probabilistic) setting (e.g. Hoare logics) in some context.

Deadlines and Structure

All in-person meetings will take place in the seminar room for our chair. Route description.

Date Event
TBD Kick-off meeting
TBD Paper submission (for peer-review)
TBD Submission Reviews
TBD Presentation slides submission
TBD Seminar talks
TBD Final paper submission

Topics:

  1. Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
  2. Proof rules for purely quantum programs
  3. A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
  4. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
  5. Quantum POMDPs
  6. Probabilistic Model–Checking of Quantum Protocols
  7. Model-Checking Linear-Time Properties of Quantum Systems
  8. Verifying Quantum Circuits with Level-Synchronized Tree Automata
  9. Efficient Formal Verification of Quantum Error Correcting Programs
  10. Verification of Nondeterministic Quantum Programs
  11. Reasoning about Grover’s Quantum Search Algorithm using Probabilistic wp
  12. Refinement calculus of quantum programs with projective assertions
  13. Proq: Projection-based Runtime Assertions for Debugging on a Quantum Computer
  14. Bayesian Inference in Quantum Programs