Vérifier automatiquement la correction des utilisations et des implémentations de librairies de collections – VECOLIB

Notre société moderne a besoin de plus de services automatisés et, par
conséquent, de logiciels performants. Pour répondre à ce besoin, la
plupart des langages de programmation offrent des librairies de
containeurs afin d'abstraire les détails des implémentations,
concernant la manipulation de données.

Notre projet a pour but l'analyse de logiciels, considérant deux
niveaux d'abstraction: (1) un haut niveau de spécification, utilisant
des spécifications abstraites de containeurs, et (2) un bas niveau
d'implementation qui vise les détails des manipulations de la mémoire.

On envisage le développement de (a) procédures de décision pour des
logiques sur des structures de données complexes, (b) outils de
vérification utilisant le model checking et l'analyse statique, et (c)
l'inference automatique de relations de raffinement entre
spécifications et implémentations. Nos techniques seront implémentées
dans des outils prototypes qui seront testées sur des logiciels de
taille industrielle.