Différences

Cette page vous donne les différences entre la révision choisie et la version actuelle de la page.

Lien vers cette vue

free_software_for_formal_verification [Le 20/12/2012 à 16:31]
david_mentre [Free software tools for formal verification of computer programs] changement de version
— (Version actuelle)
Ligne 1: Ligne 1:
-====== Free software tools for formal verification of computer programs ====== 
  
-by  [[david_mentre|David Mentré]] <dmentre @ linux-france.org> 
- 
-//Version 2.3- 2012-12-20// 
- 
-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 as made a lengthy paper on [[http://www.dwheeler.com/essays/high-assurance-floss.html|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 : 
-    *  [[smtsolvers|SMT Solvers]] 
-    *  [[proof_assistants|Proof assistants]] 
-    *  [[model_checkers|Model checkers]] 
-    *  [[program_dev_check_environments|Environments to develop and check programs]] 
-    *  [[formal_models_environments|Environments to make and check formal models]] 
- 
-===== Conclusion ===== 
- 
-I have tested some of those software. [[http://bentobako.org/david/blog/index.php?category/Software-Verification-V%C3%A9rification-de-logiciel|See my blog for details]]. 
 
free_software_for_formal_verification.1356017511.txt.gz · Dernière modification: Le 20/12/2012 à 16:31 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ó