Loading Seminars

« All Seminars

Certifying Statistical Robustness in Coq

December 13 (2023) @ 3:00 pm - 4:00 pm

Robustness properties are a class of statistical properties that specify that perturbations in the input data should not significantly affect the result of a statistical method.  In this presentation, we explore our work in verifying claims robust mean estimators in Coq, from the seminal work of Tukey in the 1960s showing robustness bounds for the trimmed mean algorithm, as well as ongoing work in verifying more recent claims of robustness.  In the process, we have contributed new probability lemmas of the coq-infotheo library for information theory, and — in order to better handle the probability theory of more advanced algorithms — we present a new library for probability theory based on Lebesgue Measure theory that is being integrated into MathComp-analysis.

This is a joint seminar with FM-SEC.

Attendance via Zoom (TBA)
Livestream via Youtube (TBA)


December 13 (2023)
3:00 pm - 4:00 pm


Alessandro Bruni (ITU)

Alessandro Bruni is Associate professor at the IT-University of Copenhagen, member of the Center for Information Security and Trust. His research focusses on formal methods applied to the verification of security protocols and AI.

View Presenter Website