Quantitative Reasoning Methods for Probabilistic Logics – QuaReMe

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 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.