Modèles mémoires collaboratifs pour la vérification formelle – CoMeMoV

Frama-C a été utilisé avec succès pour la vérification déductive dans de nombreuses études de cas. De récentes applications conduites à Thales Research & Technology ont montré le besoin d'améliorations importantes afin de permettre de vérifier efficacement et de manière correcte des logiciels industriels de plus de 10000 lignes de code mêlant des structures de données complexes, de l'allocation dynamique de mémoire, et des constructions de bas-niveau telles que des champs de bits. Le greffon WP de Frama-C fournit une combinaison de différents modèles mémoire qui collaborent grâce à une partition simple mais pertinente de la mémoire en différentes régions. Sur des programmes de complexité modérée, cette approche a montré sa maturité dans la vérification de programme critiques embarqués industriels. Toutefois, plusieurs problèmes théoriques et pratiques restent à résoudre. L'objectif de CoMeMov est de les surmonter pour passer à l’échelle sur des programmes de grande complexité.