La page de Dawson Engler à Stanford, un des fondateurs de Coverity, contient des références vers des papiers sur le sujet : http://www.stanford.edu/~engler/(...) .
Ces outils d'analyse statique du code peuvent donc s'appliquer sur du code réel, éventuellement annoté. Ceci le rend utilisable relativement aisément sur de grands projets.
Pour aller plus loin, il faut passer par de la vérification formelle, dont l'objectif est de prouver formellement le fonctionnement correct du logiciel. David Mentré maintient sur http://www.gulliver.eu.org/ateliers/fv-tools/fv-tool-list.html(...) une liste de ces outils. Évidemment, ils sont beaucoup plus lourds à utiliser sur de gros projets, et sont pour l'instant réservés à des applications vraiment critiques.
[^] # Re: Tests sur la sécurité du code
Posté par Thomas Petazzoni (site web personnel) . En réponse à la dépêche Démarche qualité et Logiciel Libre. Évalué à 3.
Un ancien article de Linux Weekly News parle également de l'analyse statique de code pour le noyau : http://lwn.net/Articles/87538/(...) .
La page de Dawson Engler à Stanford, un des fondateurs de Coverity, contient des références vers des papiers sur le sujet : http://www.stanford.edu/~engler/(...) .
Ces outils d'analyse statique du code peuvent donc s'appliquer sur du code réel, éventuellement annoté. Ceci le rend utilisable relativement aisément sur de grands projets.
Pour aller plus loin, il faut passer par de la vérification formelle, dont l'objectif est de prouver formellement le fonctionnement correct du logiciel. David Mentré maintient sur http://www.gulliver.eu.org/ateliers/fv-tools/fv-tool-list.html(...) une liste de ces outils. Évidemment, ils sont beaucoup plus lourds à utiliser sur de gros projets, et sont pour l'instant réservés à des applications vraiment critiques.