L'objectif de notre projet de recherche est de développer une technologie nouvelle pour pouvoir vérifier de manière automatique des programmes comportant un contrôle et une structure de mémoire dynamiques et non-bornés.
A titre d'exemple et sans soucis d'exhaustivité, cette technologie devrait permettre la vérification automatique des propriétés liées à l'accès à des configurations illicites du contrôle et de certaines zones de la mémoire, à l'existence de mémoire allouée qui n'est plus utilisée et qui pourrait être libérée par un GC, à l'existence de code inaccessible qui ne sera jamais exécuté ou de code redondant, ainsi que la prise en compte des contraintes à la fois temporelles et spatiales dans l'ordonnancement, etc.
Un système logiciel peut comprendre plusieurs des aspects mentionnés ci-dessus, voire tous, simultanément. Il est alors nécessaire que la vérification tienne compte des combinaisons dont les effets sont fortement interdépendants. Par exemple, la vérification de propriétés sur la structure de la mémoire ou sur la consommation de ressources mémoire ne peut ignorer la possibilité de création dynamique de processus parallèles ou celle d'avoir des appels récursifs de procédures, comme elle ne peut se passer d'intégrer un raisonnement sur les valeurs possibles des paramètres et des variables manipulées.
En particulier, le programme de recherche se déroulera selon les axes suivants: