Proving programs : why, when and how ?

This year's lecture inaugurates a multi-year cycle dedicated to the formal development of programs and circuits. Its main focus will be the study of formal verification methods and tools, which seek to establish mathematical proofs of total correctness (the realization implements the whole specification and nothing but it) or partial correctness (certain types of bugs cannot occur). The associated techniques are based on a variety of mathematical and algorithmic approaches. They are implemented in verification systems ranging from research prototypes to industrial tools actually used routinely in specific industrial fields.

The development of software or circuits is traditionally based on a top-down working model, from design to implementation, then moving upwards from unit testing of software components to integration testing. Application validation is thus based exclusively on test sets, often developed by hand according to informal specifications. This method is reasonably effective for programs that take fairly uniform data at the start of execution and return results at the end of execution. But it often proves inadequate for programs where bugs can have formidable direct or indirect consequences: those with highly varied inputs, such as compilers which have to reject or correctly translate all possible programs; programs which act in permanent interaction with their environment, such as operating systems and web-based distributed applications; reactive programs used to control cyber-physical systems which interact in real time with a complex physical environment (transport, robots, etc.); subtle protocols which ensure the correct operation of a program; and, last but not least, programs which are used to control a complex physical environment.), the subtle protocols that ensure computer security, electronic voting systems and so on. The conditions of execution can then be extremely numerous and completely untestable. What's more, while testing can validate behavior or detect bugs in the execution conditions actually examined, it says absolutely nothing about the others.

The idea of going much further, by replacing testing with a truly formal verification of behavior for all possible inputs, goes back to an article by Alan Turing in 1949. In it, he proposed that programs, their data and results should be seen as mathematical objects, and that the question of their correctness should be raised mathematically. This proposal was subsequently taken up and amplified by numerous authors. First of all, it requires a formal definition of the languages in which programs are written, a subject covered extensively in previous lectures. Next, it is necessary to formally specify which inputs the application can receive and which behaviors it must exhibit, and then to develop the appropriate proof methods. Since "hand-written" proofs can only be applied to small programs, it is essential to build them in a computerized way, using fully automatic systems or wizards that minimize human intervention depending on the case (this is the notion of "calculus on calculus" that I already presented in my 2009-2010 lecture). As it is not always possible or realistic to specify or prove everything, we settle for a balance between the critical properties to be proven and those for which the test remains reasonable in practice. But some approaches go further, by fully integrating specification, programming and proof in a stepwise development where specifications are refined into implementation, with each refinement step being proved. More recently, in a breathtaking piece of work by Georges Gonthier and his team, the formal verification techniques implemented in the Coq system developed at Inria have made it possible to produce truly formal proofs of major mathematical theorems such as the 4-color theorem or the weighty Feit-Thompson theorem on the classification of odd-order finite groups.

All work on formal verification has come up against difficult fundamental questions as much as the complex realization of the associated software. They gave rise to a remarkable number of Turing awards, the highest distinction in computer science: John McCarthy (1971), Edsger Dijkstra (1972), Dana Scott (1976), Robert Floyd (1978), Charles A. R. Hoare (1980), Robin Milner (1991), Amir Pnueli (1996), Edmund Clarke, Allen Emerson and Joseph Sifakis (2007) and Leslie Lamport (2013), as well as numerous other awards for French researchers: Thierry Coquand, Patrick Cousot, Gorges Gonthier, Gérard Huet, myself, etc. They have helped to prove numerous industrial systems, and considerably increased the quality of associated programs and circuits. But the technical nature of the subject and its close links with the fragmented landscape of programming languages have meant that work in formal verification has often taken place in communities that remain separate, which does not simplify a unified presentation. The situation is improving as recent verification systems increasingly seek to combine various verification methods, thereby simplifying the landscape and improving the applicability of formal verification to real systems.

Proving programs : why, when and how ?

Documents and media

Program

The computer revolution in science

From specification to realization, testing and proof : formal approaches

The Internet of Things, a revolution not to be missed

General methods : assertions, rewriting, abstract interpretation, logics and proof assistants

Using formal methods to secure complex systems : an industrial breakthrough

Logics of higher order than programming verified in Coq

Languages and systems for interactive proof

Model-checking

Proving IT security : logic to the rescue

Boolean verification and optimization of PLCs and circuits

Program specification, construction and verification : the path of scientific thought over forty years

See also