CAVALE

La vérification de code embarqué critique est aujourd'hui essentiellement effectuée par analyse dynamique sous la forme de jeux de test. Les méthodes formelles d'analyse statique seront amenées à jouer un rôle de plus en plus important, compte tenu de l'augmentation de la taille des systèmes ainsi que des exigences de certification. Chaque méthode (interprétation abstraite, preuve de propriété par calcul de plus faible précondition, etc) possède ses forces et ses faiblesses propres et nécessite une mise en oeuvre spécifique. L'objectif de ce projet est double. Il s'agit d'une part d'étudier et de proposer un cadre pour la collaboration d'analyses statiques afin d'en améliorer la précision et d'en faciliter le passage à l'échelle; et d'autre part de permettre une intégration harmonieuse de ces analyses dans les processus de validation et vérification utilisés actuellement.