Cadre algébrique pour l'analyse de programmes informatiques

点击翻译按钮获取中文摘要

L'analyse de programmes est un domaine de l'informatique dans lequel on vise à produire des outils automatiques et semi-automatiques qui permettent d'avoir une meilleure compréhension de ce que fait un code. Par exemple, grâce à l'analyse de programmes, il est possible de vérifier qu'un programme est conforme à une politique donnée, de vérifier qu'une version optimisée ou obscurcie d'un programme est sémantiquement équivalente à sa version originale, et d'instrumenter un programme par insertion ou modification de code pour contraindre son comportement à être conforme à une politique. Dans le contexte actuel, où de plus en plus de logiciels sont distribués et mis à jour par Internet, il est nécessaire de disposer de tels outils afin d'analyser les programmes avant qu'ils ne soient installés sur nos machines, et ultimement, de «corriger» leur comportement pour les contraindre à respecter nos politiques.