Verifying Probabilistic Programs with Separation Logic

Lectures by Joseph Tassarotti (New York University).
11–15 May 2026, EPIT 2026, CIRM, Marseille, France.

This page collects materials for the EPIT 2026 lectures on Verifying Probabilistic Programs with Separation Logic.

Software setup

To set up for following along with the lectures::

1. Clone the logsem/clutch repository to your machine. From a terminal, in the directory where you want the clutch folder to live, run:
   

   git clone https://github.com/logsem/clutch.git
   cd clutch
   git checkout epit2026
   

2. Follow the instructions in the Building the development section of the Clutch README.
3. (Optional) Set up the VS Code Dev Container by following the Visual Studio Code section of the README.

Slides

• Part 1 slides
  • Background on modern separation logic and Iris: Hoare triples, points-to, the frame rule, persistent modality, magic wand, weakest preconditions, later modality and Löb induction.
  • Probabilistic preliminaries: distributions, a probabilistic language and its operational semantics, with small examples.
  • A comparison of three approaches to probabilistic program logics: distributional assertions, expectation transformers, and lifting-based logics.
  • Introduction to Eris and error credits for “up-to-bad” reasoning.
• Part 2 slides
  • A worked example based on Morris's approximate counter, developed through three progressively tighter specifications.
  • Almost-sure termination with Eris_t.
  • An error-credit induction principle for proving almost-sure termination.
• Part 3 slides
  • Pitfalls of floating-point sampling (e.g. Mironov's attack on ε-differential privacy) motivating exact sampling via computable reals.
  • Verifying continuous samplers with Continuous-Eris. Using presampling tapes for reasoning about sampled values ahead of time.
  • Relational reasoning: contextual equivalence and refinement, logical relations, and couplings in Clutch

Background reading

Optional: See the Logics and Examples page and the Publications list for an overview of the larger family of logics that includes the ones we'll be studying.