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