En principe, un outil d'analyse statique doit être prouvé formellement. En effet, il est inutile de vérifier un programme par un autre programme si les deux sont potentiellement aussi faux l'un que l'autre. Autant passer du temps en relecture de code. On doit donc déterminer le type d'analyse qu'on doit effectuer et les propriétés qu'on veut étudier et démontrer formellement (mathématiquement) que cette analyse fonctionne.
Le problème, c'est qu'il faut définir premièrement la sémantique du programme, c'est à dire du langage de programmation utilisé et deuxièmement, il faut se rendre compte que cette analyse est "moins précise" qu'une exécution exhaustive de tous les états possibles du programme, qui est infiniment précise mais aussi potentiellement infiniment longue. On doit donc s'assurer que notre représentation "moins précise" permet une analyse en temps fini et que les résultats ont encore un sens dans le programme réel : c'est un compromis pas toujours simple.
Tout ça pour dire que la plupart des analyseurs statiques du marché ont un noyau correctement prouvé, mais qu'on fait aussi pas mal de compromis pour obtenir un résultat raisonnable.
[^] # Re: SWAT exempté?
Posté par Germain Saval . En réponse à la dépêche 985 bugs dans le noyau Linux. Évalué à 5.
Le problème, c'est qu'il faut définir premièrement la sémantique du programme, c'est à dire du langage de programmation utilisé et deuxièmement, il faut se rendre compte que cette analyse est "moins précise" qu'une exécution exhaustive de tous les états possibles du programme, qui est infiniment précise mais aussi potentiellement infiniment longue. On doit donc s'assurer que notre représentation "moins précise" permet une analyse en temps fini et que les résultats ont encore un sens dans le programme réel : c'est un compromis pas toujours simple.
Tout ça pour dire que la plupart des analyseurs statiques du marché ont un noyau correctement prouvé, mais qu'on fait aussi pas mal de compromis pour obtenir un résultat raisonnable.