Le greffon Synchrone de Frama-C est dédié à l'analyse de programmes Lustre. Il combine les capacités des greffons WP et Eva et communique avec le solveur GaTeL pour prouver diverses propriétés à propos des programmes sous analyse. Les travaux de ce postdoc visent à améliorer l'usage global de Synchrone à travers cet ensemble de challenges scientifiques:
- développer une méthodologie de vérification qui tire parti de la combinaison de techniques disponibles au sein de l'outil, notamment en l'appliquant à des cas représentatifs de l'usage réel de Synchrone,
- pour supporter cette méthodologie, améliorer l'outillage disponible au sein de synchrone, notamment en ce qui concerne la génération des obligations de preuves, et leur optimisation pour les solveurs automatiques, comme le solveur Colibri2 développés au sein du laboratoire,
- améliorer le lien entre ce qui est vérifié et le modèle mathématique qui spécifie le système, par l'extension du langage LustreSpec et le développement de l'outillage associé, cela comprend notamment les aspects liés à la gestion des filtres numériques,
- développement de l'outillage pour la visualisation et le déboggage des obligations de preuve.

Ce postdoc est donc plutôt orienté vers un travail d'ensemble visant des publications orientées méthodologie de vérification dans un contexte industiel.