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. Frama-C et WP n'utilisent donc pas cette logique.
Dans un travail récent nous avons décrit comment étendre l'outillage de WP pour décrire l'empreinte mémoire de structures de données en C. L'idée est d'avoir un langage de spécification capable de capturer la majorité de la puissance de la logique de séparation sans avoir à l'encoder dans les outils de preuve. Le but de ce postdoc est d'expérimenter l'usage de ce formalisme pour décrire des cas réels et d'implémenter son support au sein de Frama-C et WP.