Abstract
This first lecture in the "Proving programs: why, when, how" series aims to introduce formal methods of program development and verification, linking them to conventional programming, testing and validation methods.
From the very beginnings of computing, the difficulty of producing correct programs has been a major problem. Two very different approaches were developed: on the one hand, software engineering, which developed slowly but is now well established at least in serious companies, and, on the other, a much more scientific formal approach, introduced by Turing as early as 1949 and based on the idea of seeing a program as a mathematical entity about which one must reason mathematically. It is this latter approach that led to the formal methods we'll be studying this year and next. These two approaches developed very independently of each other, and have only recently begun to converge: formal development and verification now appear to be effective, even privileged, ways of avoiding bugs, at least in applications where their human and material cost can be catastrophic. Formal verification techniques have been slow to mature, partly because the subject is intrinsically difficult, and partly because the industry has only recently taken a real interest in them. But things are moving fast, with successes becoming more and more frequent. And, what's more, French researchers are playing a major role in this fast-growing field.
