Verification of the CVM algorithm with a functional probabilistic invariant

DOI10.4230/LIPICS.ITP.2025.34MaRDI QIDQ7323694zbMATH OpenFDO

Authors Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.34

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• An embarrassingly parallel optimal-space cardinality estimation algorithm
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Balls and bins: A study in negative dependence
• Certifying certainty and uncertainty in approximate membership query structures
• Correlation inequalities on some partially ordered sets
• Counting large numbers of events in small registers
• Distinct elements in streams: an algorithm for the (text) book
• Formalization of randomized approximation algorithms for frequency moments
• scientific article; zbMATH DE number 5763313 (Why is no real title available?)
• scientific article; zbMATH DE number 3764843 (Why is no real title available?)
• scientific article; zbMATH DE number 2019620 (Why is no real title available?)
• scientific article; zbMATH DE number 819814 (Why is no real title available?)
• Information theoretic limits of cardinality estimation: Fisher meets Shannon
• Isabelle/HOL. A proof assistant for higher-order logic
• Moment-based invariants for probabilistic loops with non-polynomial assignments
• Negative association of random variables, with applications
• Optimal streaming and tracking distinct elements with high probability
• Probabilistic counting algorithms for data base applications
• Probabilistic functions and cryptographic oracles in higher order logic
• Probabilistic program verification via inductive synthesis of inductive invariants
• Probability and computing. Randomization and probabilistic techniques in algorithms and data analysis
• Probability Inequalities for Sums of Bounded Random Variables
• Proofs of randomized algorithms in Coq
• The probabilistic method. With an appendix on the life and work of Paul Erdős.
• The space complexity of approximating the frequency moments
• Verified analysis of list update algorithms
• Verified analysis of random binary tree structures
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC

This page was built for publication: Verification of the CVM algorithm with a functional probabilistic invariant

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323694)