Le projet SLAM a débuté à Microsoft Research début 2000. Son but était de vérifier automatiquement qu'un programme C utilise correctement l'interface d'une bibliothèque extérieure. Pour répondre à cette question, SLAM utilise de manière novatrice des idées provenant de la vérification symbolique de modèles, de l'analyse statique de programmes et de la démonstration automatique. Le moteur d'analyse SLAM est au coeur d'un nouvel outil appelé SDV (Vérification Statique de Drivers) qui analyse systématiquement le code source des drivers (pilotes de périphériques) Windows et vérifie leur conformité vis-à-vis d'un ensemble de règles qui caractérisent les interactions correctes entre un driver et le noyau du système d'exploitation Windows.
Dans le rapport technique MSR-TR-2004-08, T.Ball, B.Cook, V.Levin and S.K.Rajamani, les auteurs de SLAM, écrivent: "The Right Tools for the Job: We developed SLAM using INRIA's OCaml functional programming language. The expressiveness of this language and robustness of its implementation provided a great productivity boost."
[^] # Re: Le retour en force du fonctionnel ?
Posté par Gilles G. . En réponse à la dépêche Ocsigen 1.0.0 : une nouvelle approche de la programmation Web. Évalué à 6.
http://caml.inria.fr/about/successes.fr.html
Le projet SLAM a débuté à Microsoft Research début 2000. Son but était de vérifier automatiquement qu'un programme C utilise correctement l'interface d'une bibliothèque extérieure. Pour répondre à cette question, SLAM utilise de manière novatrice des idées provenant de la vérification symbolique de modèles, de l'analyse statique de programmes et de la démonstration automatique. Le moteur d'analyse SLAM est au coeur d'un nouvel outil appelé SDV (Vérification Statique de Drivers) qui analyse systématiquement le code source des drivers (pilotes de périphériques) Windows et vérifie leur conformité vis-à-vis d'un ensemble de règles qui caractérisent les interactions correctes entre un driver et le noyau du système d'exploitation Windows.
Dans le rapport technique MSR-TR-2004-08, T.Ball, B.Cook, V.Levin and S.K.Rajamani, les auteurs de SLAM, écrivent: "The Right Tools for the Job: We developed SLAM using INRIA's OCaml functional programming language. The expressiveness of this language and robustness of its implementation provided a great productivity boost."