When programs prove themselves
Claude Marché, Toccata team leader - © Inria / Photo Kaksonen
In 2013, eight years after the creation of the Proval team headed by Christine Paulin-Mohring, the team has reached a turning point. Today it has taken on new directions and a new manager, Claude Marché. Claude tells us more about this new team, Toccata.
What is the team's field of research and what avenues are you pursuing?
In the Toccata team, we are working on proof of program correctness. In the Proval team, our research was concerned mainly with designing programs to verify other programs. Today, we wish to pursue the verification of the verification tools themselves.
In concrete terms, Toccata’s work is divided into three avenues of research:
- proof of verification tools. These tools are generally concerned with symbolic computation (compilers, proof obligation generators, automated theorem proving). As such, we think they make ideal areas to put our approaches to formal verification by specification and computer-assisted proof into application.
- verification of programs that perform digital computation. We want to be capable of certifying systems that function on the basis of applied mathematics, in particular differential equations. You can't model physical systems without the help of mathematics, which is then translated by differential equations. The solutions arrived at through computer equations such as these are complex programs, and we naturally want to verify that they function correctly. One special feature of our team is that we are able to apply mathematical reasoning just as well with regard to errors in the solution method as to errors arising from rounding in the calculations.
- lastly, one traditional avenue of research, which was the foundation of the Proval team, is automated demonstration. This means examining the specification on the one hand, and looking at the program designed to respond to it on the other. Then we verify the match. To do that, you need to be able to feed a theorem into a computer so that the computer says "This theorem is true". In this way, we are looking to have tools that are both powerful and suitable for proof of program correctness.
What is proof of program correctness?
When we talk about proof of program correctness, we hear the words "proof", which suggests mathematics, and "program" which suggests computing. So what is a program? A program is a series of texts (lines of code) written on a computer by a programmer. The computer then interprets that code to make the software work. In simple terms, the programmer explains to the computer what the software is supposed to do. So, we could say that program is the original description, and the software is the final product.
There are programs written for the tools we use in our everyday lives, such as when we surf the Web, send an email, use a word processor, and so on. Then there are programs that make machines like aircraft and cars work properly. Only those used to dealing with them can interact with programs of that sort: there's no mouse, no keyboard, no windows for graphic representations. And yet, these programs are constructed in the same way, whatever the software they are designed for. Using a compiler, the programming language is translated into binary code, the language understood by the computer, so the computer can then execute the program.
And proof of program correctness?
We want to be sure that the program does what the programmer told it to do. To this end, we consider that the programmer gave the computer a set of specifications, a bit like the technical specifications for a building project. To take an example from aviation, this would mean specifying that the speed must not be less thanxkm/h, and that the aircraft must never be less thanykm from any other aircraft, in order to avoid the risk of collision. Or if we take the example of an automated subway system, it would be the specification that the doors must not open unless the train is stationary at the platform. So, the specifications are all the pieces of information that we need to make the rules that govern correct function.
Program verification, or proof of program correctness, therefore consists of using other programs to examine all of the specifications of a newly written program, to see if they work, or contain errors that would affect the proper functioning of the software.
At Inria's Saclay centre, several teams are working on this subject and offer different methods of program verification. Our team has proposed verification by formal proofs, in much the same way that mathematical theorems are proved. Formal computer-assisted proofs are already an established speciality for Inria. This is how the Coq program came about (developed by several Inria teams), which is used to prove mathematical theorems, like the four colour theorem, or more recently the Feit/Thompson theorem. It can also be used for proof of program correctness, like the CompCert compiler.
What are the applications of proof of program correctness?
The team's research avenues are both theoretical (mathematical, if you will) and at the same time practical. We look to provide methods that have industrial applications, particularly for the aviation industry, as that is where certification constraints are the most stringent. It is also where the most money is invested to ensure proof of program correctness. Several methods for proving program correctness have been proposed to manufacturers in the aircraft industry (Dassault Aviation, Airbus).
But here a new problem arises: the tools used by these manufacturers have to certified, i.e. they have to be able to convince the certifying bodies responsible for civil aviation that the development methods and the tools they use really work. This process involves writing up exhaustive texts to convince the certifier that the program does indeed give the correct answers. To date, only the team's Alt-Ergo tool has been certified and put into use by manufacturers. We hope that the verification of the verification tools themselves, which is what we offer in the Toccata team, will make for a less complex qualification process.