C'est d'ailleurs pour cela que cet nouvelle feature, va permettre à krosoft de proposer de la vérification statique à la compilation, par model checking, ou peut être une espèce d'analyse de flot sur le code de la machine virtuelle (mais j'y crois moins).
Microsoft fournit déjà avec son kit de développement de pilotes un outil baptisé SLAM, combinant analyse statique par interprétation abstraite, démonstration automatique et model-checking pour détecter d'éventuelles erreurs dans le code du pilote. D'après ce que j'ai entendu dire, il s'agit d'une mise en pratique de l'état de l'art de ces différents domaines. D'après Wikipédia, il est (était ?) écrit en OCaml, langage développé en France à l'INRIA. Cocorico !
# Microsoft et analyse statique
Posté par auve . En réponse au journal Contrats et exceptions. Évalué à 4.
C'est d'ailleurs pour cela que cet nouvelle feature, va permettre à krosoft de proposer de la vérification statique à la compilation, par model checking, ou peut être une espèce d'analyse de flot sur le code de la machine virtuelle (mais j'y crois moins).
Microsoft fournit déjà avec son kit de développement de pilotes un outil baptisé SLAM, combinant analyse statique par interprétation abstraite, démonstration automatique et model-checking pour détecter d'éventuelles erreurs dans le code du pilote. D'après ce que j'ai entendu dire, il s'agit d'une mise en pratique de l'état de l'art de ces différents domaines. D'après Wikipédia, il est (était ?) écrit en OCaml, langage développé en France à l'INRIA. Cocorico !
* : http://research.microsoft.com/en-us/projects/slam/
* : http://caml.inria.fr