Raphaël Rieu-Helft presented his paper at Oxford University
Why3 framework for reflection proofs and its application to GMP’s algorithms
Employee Presentation at International Joint Conference on Automated Reasoning
Our employee Raphaël Rieu-Helft attended the 9th International Joint Conference on Automated Reasoning, within the Federated Logic Conference at the prestigious Oxford University.
There, he presented “A Why3 framework for reflection proofs and its application to GMP’s algorithms” co-authored with Guillaume Melquiond from Inria. This framework makes it easier to write dedicated decision procedures that make full use of Why3’s imperative features and are formally verified. Raphaël uses it to formally verify GMP’s algorithms.
Have a look at his presentation here
As we are always striving for continuous scientific improvements, we are truly proud of Raphaël’s achievement.
CONGRATULATIONS Raphaël!
