Interval Normal Jordan Form
Un point difficile lors de l’analyse statique d’un programme est le traitement des boucles.
- Dans l’interprétation abstraite de Cousot et Cousot, l’approche traditionnelle est de définir un opérateur d’élargissement pour inférer assez précisément ce qui se passe au bout de nombreux tours de boucles.
- Des approches plus modernes, comme celle de Jeannet et al., utilisent la mise sous forme normale de Jordan de matrices pour capturer très précisément l’effet de n tours de boucles. Cette opération est très coûteuse.
- Le logiciel IJNF, que j’ai élaboré avec Marc Pasqualetto, propose une version approximée mais efficace pour la mise sous forme normal de Jordan. Les coefficients sont approximés par un intervalle de variation.
Graph Based Static Analysis
En analyse statique de programme par interprétation abstraite, l’analyse s’effectue traditionnellement par itération sur l’arbre de syntaxe abstrait du programme.
Bourdoncle et Jeannet se sont penchés sur la possibilité d’effectuer l’analyse sur une représentation du programme comme un graphe.
La bibliothèque GBSA permet de développer de telles analyses statiques en OCaml, en fournissant tout l’aspect lié aux graphes. Elle s’inspire largement de la biblothèque FixPoint de Jeannet, mais dans un style purement fonctionnel.