DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.71

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Authors: Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, and Joseph Tassarotti

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state. In this paper we present Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we verify the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples. All of the results in this paper have been verified in the Rocq proof assistant.

Cite as

Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, and Joseph Tassarotti. Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 71:1-71:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{demedeiros_et_al:LIPIcs.LICS.2026.71,
  author =	{de Medeiros, Markus and Liu, Puming and Li, Kwing Hei and Aguirre, Alejandro and Birkedal, Lars and Tassarotti, Joseph},
  title =	{{Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{71:1--71:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.71},
  URN =		{urn:nbn:de:0030-drops-268584},
  doi =		{10.4230/LIPIcs.LICS.2026.71},
  annote =	{Keywords: Probabilistic Programming, Separation Logic, Formal Verification}
}

Document

DOI: 10.4230/DagRep.13.10.50

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)

Authors: Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, and Anton Podkopaev

Published in: Dagstuhl Reports, Volume 13, Issue 10 (2024)

Abstract

Recently developed non-volatile memory (NVM) devices provide persistency guarantees along with byte-addressable accesses and performance characteristics that are much closer to volatile random-access memory (RAM). However, writing programs that correctly use these devices is challenging, and bugs related to their use can cause permanent data loss in applications. This Dagstuhl Seminar brought together experts in a range of areas related to concurrency and persistent memory to explore and develop formal methods for ensuring the correctness of applications that use persistent memory. Talks and discussions at the seminar highlighted challenges related to correctness criteria for concurrent objects using persistent memory, liveness properties of persistent objects, and how changes in NVM and related technologies should shape the development of formal methods for NVM.

Cite as

Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, and Anton Podkopaev. Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). In Dagstuhl Reports, Volume 13, Issue 10, pp. 50-64, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{lahav_et_al:DagRep.13.10.50,
  author =	{Lahav, Ori and Raad, Azalea and Tassarotti, Joseph and Vafeiadis, Viktor and Podkopaev, Anton},
  title =	{{Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)}},
  pages =	{50--64},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{10},
  editor =	{Lahav, Ori and Raad, Azalea and Tassarotti, Joseph and Vafeiadis, Viktor and Podkopaev, Anton},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.50},
  URN =		{urn:nbn:de:0030-drops-198337},
  doi =		{10.4230/DagRep.13.10.50},
  annote =	{Keywords: concurrency, formal methods, non-volatile-memory, persistency, verification}
}

Search Results

Documents authored by Tassarotti, Joseph

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Abstract

Cite as

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)

Abstract

Cite as

Thanks for your feedback!

Could not send message