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