View article

Program verification is a branch of computer science whose business is" to prove programs correctness". It has been studied in theoretical computer science departments for a long time but it is rarely and laboriously applied to real world problems. As a matter of fact, we must pay much more attention to practical problems like the amount of space and time needed to perform verification. Let us recall that proofs of correctness are proofs of the relative consistency between two formal specifications: those of the program, and of the properties that the program is supposed to satisfy. Such a formal proof tries to increase the confidence that a computer system will make it right when executing the program under consideration.

A considerable need for such methods appeared these last ten years in different domains, such as design of asynchronous circuits, communication protocols and distributed software in general. A lot of …