Colloquium Loria : next talk with Xavier Leroy
3 May 2018
Xavier Leroy, research director at Inria Paris is the guest of the upcoming Loria’s Colloquium.
Appointment on Friday, May 25 at 1:30 pm in the amphitheater to listen to his presentation entitled “In Search of Software Perfection”
The talk will be in French.
For the general public, the word “software” has become synonymous with “bug” and “security breach”. Yet, there are critical software, on which human lives depend, that reach an extraordinary level of reliability.
Taking the example of avionics electronic flight control software, I will show some of the techniques that lead to this reliability. One of these involves the use of formal methods automated by verification tools (static analysis, proof of programs, verification by models) in addition to, and sometimes replacing, traditional methods of verification based on tests. .
However, the guarantees provided by the formal verification are limited by the confidence we can have in the verification tools and to the compilers and automatic code generators that produce the real executable code from the source code that has been verified. Based on the example of CompCert verified C compiler, I will show the interest and efficiency of formally verifying, with the aid of proof assistants, the tools that are involved in the construction and verification of the software.
For people whose not member of Loria, thank you for registering by e-mail before Tuesday, May 22.