Frama-C est une plateforme collaborative pour l'analyse de programmes écrits en C. Parmi les outils proposés au sein de Frama-C, WP est dédié à la vérification déductive de programme, qui permet la preuve mathématique de propriétés fonctionnelles et l'absence d'erreurs à l'exécution. Cet outil est utilisé depuis des années dans l'industrie.
La logique de séparation est la voie la plus prometteuse pour permettre la preuve de propriétés sur des programmes manipulant des structures de données complexes. Cependant, il est difficile de l'utiliser pour des études de cas industrielles. La principale raison à cela est la difficulté pour l'encoder vers des outils de preuve automatique. Aussi, son utilisation nécessite beaucoup de travail de la part de l'utilisateur.
L'outil WP de Frama-C n'utilise pas la logique de séparation. Un projet de recherche actuel vise à intégrer certains éléments de logique de séparation pour augmenter les performances et les capacité de WP à traiter des structures complexes. Cependant, l'extension proposée ne permet pas de traiter des structures récursives, pour cela les prédicats de représentation de la logique de séparation doivent être ajoutés. Le but de ce postdoc est d'étudier l'intégration de ces prédicats à WP.