Vérification dynamique ciblée et interactive de programmes grâce à une architecture modulaire

Le cycle de développement d'une application contient plusieurs phases, de l'écriture au soutien technique suivant la publication. Une phase particulièrement importante est la vérification du programme. Il s'agit de vérifier que le programme produit répond à la spécification au sens large, c'est à dire qu'il présente le comportement prévu sans bogue, quel que soit le scénario et les entrées présentées. De nombreux outils sont disponibles pour assister l'utilisateur dans cette tâche. Parmi ceux-ci, on trouve les outils de vérification formelle qui permettent de modéliser le déroulement d'un programme et d'en prouver mathématiquement la validité. Les analyses statiques peinent cependant à vérifier des programmes complexes, et une autre famille d'outils est souvent nécessaire. Ce sont les outils dynamiques, qui vérifient l'intégrité du programme pendant son exécution. Dans ce domaine, on trouve surtout des outils spécialisés et efficaces, mais peu flexibles. En effet, en l'absence d'une structure commune, beaucoup d'outils réécrivent intégralement toutes les fonctionnalités de base, et ce coût de développement fait qu'ils se limitent souvent aux fonctionnalités strictement nécessaires. Peu d'outils proposent ainsi une instrumentation dynamique ou une interface graphique.