We are now living in 2004. We should no longer make software as in the sixties or seventies, with a few tests. We are now able to make software without any bugs. This is possible using specialised tools called formal tools. Such tools are able to match a computer program against a specification, i.e. a formal description of the expected behavior of the program. If the specification is correct and the formal verification can be done, then the program is guaranted to be bug free.

Of course, this is the ideal case and we are far from guaranteed bug free programs in the real world. But, as developer of free software, we should try to be as close as possible of this goal.

I intend to put on this page pointers and documentation on how to use those tools to improve free software.

As a first step, I list here free software tools that can help verification of computer programs (PDF version, TeXmacs source).

You can contact me at dmentre@linux-france.org if you want to contribute to this project or for further information.

You'll find a lot of useful information at the Formal Methods Virtual Library