Matteo Mio
PhD, CNRS Researcher

---

QuaReMe: Quantitative Reasoning Methods for Probablistic Logics.

This is the reference page of the project QuaReMe, funded by the french ANR. Some informations:

• Acronym: QuaReMe
• ANR Code: ANR-20-CE48-0005
• Instrument de financement : JCJC - Jeunes chercheurs - jeunes chercheuses
• Duration: 48 months 60 months
• Start date: 10/2020
• End date: 09/2024 09/2025
• Research centers involved: ENS-Lyon (LIP), Universite de Paris (IRIF)

Abstract: The goal of this project is to advance the state of the art regarding techniques for formally proving the correctness of programs that use probabilistic operations such as, e.g., random number generation. Importantly, our techniques will be quantitative, expressing numerical (R) properties of programs rather than, as more customary in logic, Boolean (true, false) properties. This will allow several familiar ideas from analysis, such as approximation and convergence, to be used in the context of formal verification. Our ambition is to exploit these ideas to: (A) attack some long–standing open problems in the field which have been explored so far mostly only using classical methods based on Boolean semantics, (B) design new proof systems to conveniently prove quantitative properties of programs and (C) implement these proof systems using the Coq proof assistant, allowing for practical applications of our work to emerge.

Permanent researchers involved:

• Matteo Mio (coordinator), ENS-Lyon (LIP)
• Damien Pous, ENS-Lyon (LIP)
• Olivier Laurent, ENS-Lyon (LIP)
• Alexis Saurin, Universite de Paris (IRIF)

Other researchers/students involved:

• Valeria Vignudelli (Postdoc, LIP, ENS-Lyon)
• Alexandre Goy (Postdoc, LIP, ENS-Lyon)
• Christophe Lucas (PhD student, LIP, ENS-Lyon)
• Ralph Sarkis (PhD student, LIP, ENS-Lyon)