log in  |  register  |  feedback?  |  help  |  web accessibility
Formal Methods for Randomized Concurrent Algorithms
Noam Zilberstein - Cornell University
Thursday, November 20, 2025, 12:00-1:00 pm
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

For decades, randomization has played a central role in distributed computing, offering elegant and practical solutions to problems that are difficult or impossible to solve deterministically. Applications include consensus, synchronization, and leader election algorithms that are increasingly crucial to decentralized systems such as databases and Cryptocurrency exchanges. But despite their prevalence, randomized distributed algorithms are notoriously difficult to reason about, as unexpected behavior arises from the interaction between random sampling and concurrent execution. Informal reasoning and pen-and-paper proofs often overlook those subtleties, leading to incorrect arguments and bugs. In this talk, I will outline the challenges and pitfalls behind randomized concurrent algorithms, and introduce a new foundational program logic for reasoning about such programs.

This talk is organized by Finn