David Monniaux - Software verification for fun and profit

12:00
Jeudi
7
Mai
2015
  • Keynote Speech
Lieu : 
Organisé par : 
L’équipe "Keynotes" du LIG
Intervenant : 
David Monniaux

 

David Monniaux defended his PhD in 2001 and has since 2002 been working at CNRS, first in Paris then at the VERIMAG laboratory in Grenoble where he is senior researcher. He also teaches at École polytechnique in Paris.

He was one of the developers of the Astrée static analyzer (then academic, now a commercial product). He is now principal investigator of an ERC research grant on new approaches to the static analysis of programs, focusing on relationships between numeric and "logical" information and on implicit representations.
 
 
"Réalisation technique : Djamel Hadji | Tous droits réservés"

We are used to software crashing or misbehaving in various ways. Scientists have tried to mathematically prove the correctness software for forty years now, but this endeavour was long thought to be a purely academic pastime, not scalable to real applications.

 
Here I will describe the main approaches of program verification and how the state of the art has considerably been improved in the last 15 years, to the extent that fully automated verification is possible for certain properties on large scale industrial applications such as fly-by-wire aircraft controls.
 
Two crucial points of interest to theoretically-oriented computer scientists are 1) that simple classes of arguments are sufficient to prove interesting properties on large programs 2) that the worst-case of exponential algorithms might not occur (and that if it occurs, we can work around it).