The paper introduces Eris, a novel higher-order separation logic designed to provide precise error probability bounds for probabilistic programs. By introducing the concept of error credits as a resource within the logic, the authors enable more accurate and modular reasoning about errors, improving upon existing verification approaches that often yield overly coarse bounds. This innovative method is demonstrated through applications such as analyzing collision probabilities in hash functions and proving the correctness of rejection sampling algorithms. The results have been fully mechanized in the Coq proof assistant, showcasing the robustness of the approach.

Click here to read the full paper.

Congratulations to the entire team on this outstanding achievement!