Free software tools for formal verification of computer programs

by David Mentré <dmentre@linux-france.org>

Version 3.15 2016-08-19

We are now living in the XXIst century. 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 (well, without most of them, see below). 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 behaviour of the program. If the specification is correct and the formal verification can be done, then the program is guaranteed 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. As a first step, I list here free software tools that can help verification of computer programs.

Note: David A. Wheeler has made a lengthy paper on High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods. You should read it if you are interested in the subject!

Sub-pages :

Conclusion

I have tested some of those software. See my blog for details.

 
free_software_for_formal_verification.txt · Dernière modification: Le 19/08/2016 à 21:24 par david_mentre     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó