More Like this

1. A Bayesian Proof of the Spread Lemma

   https://doi.org/10.1002/rsa.70008  

   Mossel, Elchanan; Niles‐Weed, Jonathan; Sun, Nike; Zadik, Ilias (July 2025, Random Structures & Algorithms)

   ABSTRACT A key set‐theoretic “spread” lemma has been central to two recent celebrated results in combinatorics: the recent improvements on the sunflower conjecture by Alweiss, Lovett, Wu, and Zhang; and the proof of the fractional Kahn–Kalai conjecture by Frankston, Kahn, Narayanan, and Park. In this work, we present a new proof of the spread lemma, that—perhaps surprisingly—takes advantage of an explicit recasting of the proof in the language of Bayesian inference. We show that from this viewpoint the reasoning proceeds in a straightforward and principled probabilistic manner, leading to a truncated second moment calculation which concludes the proof. 

   more » « less
2. Raven: An SMT-Based Concurrency Verifier

   https://doi.org/10.1007/978-3-031-98668-0_4  

   Gupta, Ekanshdeep; Patel, Nisarg; Wies, Thomas (July 2025, Springer Nature Switzerland)

   Abstract This paper presents , a new intermediate verification language and deductive verification tool that provides inbuilt support for concurrency reasoning. ’s meta-theory is based on the higher-order concurrent separation logic Iris, incorporating core features such as user-definable ghost state and thread-modular reasoning via shared-state invariants. To achieve better accessibility and enable proof automation via SMT solvers, restricts Iris to its first-order fragment. The entailed loss of expressivity is mitigated by a higher-order module system that enables proof modularization and reuse. We provide an overview of the language and describe key aspects of the supported proof automation. We evaluate on a benchmark suite of verification tasks comprising linearizability and memory safety proofs for common concurrent data structures and clients as well as one larger case study. Our evaluation shows that improves over existing proof automation tools for Iris in terms of verification times and usability. Moreover, the tool significantly reduces the proof overhead compared to proofs constructed using the Iris/Rocq proof mode. 

   more » « less
3. An algorithmic hypergraph regularity lemma

   https://doi.org/10.1002/rsa.20739  

   Nagle, Brendan; Rödl, Vojtěch; Schacht, Mathias (December 2017, Random Structures & Algorithms)

   Abstract Szemerédi 's Regularity Lemma is a powerful tool in graph theory. It asserts that all large graphs admit bounded partitions of their edge sets, most classes of which consist of uniformly distributed edges. The original proof of this result was nonconstructive, and a constructive proof was later given by Alon, Duke, Lefmann, Rödl, and Yuster. Szemerédi's Regularity Lemma was extended to hypergraphs by various authors. Frankl and Rödl gave one such extension in the case of 3‐uniform hypergraphs, which was later extended tok‐uniform hypergraphs by Rödl and Skokan. W.T. Gowers gave another such extension, using a different concept of regularity than that of Frankl, Rödl, and Skokan. Here, we give a constructive proof of a regularity lemma for hypergraphs. 

   more » « less
4. Sumsets and entropy revisited

   https://doi.org/10.1002/rsa.21252  

   Green, Ben; Manners, Freddie; Tao, Terence (July 2024, Random Structures & Algorithms)

   Abstract The entropic doubling of a random variable taking values in an abelian group is a variant of the notion of the doubling constant of a finite subset of , but it enjoys somewhat better properties; for instance, it contracts upon applying a homomorphism. In this paper we develop further the theory of entropic doubling and give various applications, including: (1) A new proof of a result of Pálvölgyi and Zhelezov on the “skew dimension” of subsets of with small doubling; (2) A new proof, and an improvement, of a result of the second author on the dimension of subsets of with small doubling; (3) A proof that the Polynomial Freiman–Ruzsa conjecture over implies the (weak) Polynomial Freiman–Ruzsa conjecture over . 

   more » « less
5. Toward Liveness Proofs at Scale

   https://doi.org/10.1007/978-3-031-65627-9_13  

   McMillan, Kenneth L (July 2024, Springer Nature Switzerland)

   Abstract While the problem of mechanized proof of liveness of reactive programs has been studied for decades, there is currently no method of proving liveness that is conceptually simple to apply in practice to realistic problems, can be scaled to large problems without modular decomposition, and does not fail unpredictably due to the use of fragile heuristics. We introduce a method of liveness proof by relational rankings, implement it, and show that it meets these criteria in a realistic industrial case study involving a model of the memory subsystem in a CPU. 

   more » « less