Conception et implémentation dapos;une variante des prédicats de représentation pour Frama-C

Description de l'offre : Frama-C est une plateforme collaborative pour lapos;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 lapos;absence dapos;erreurs à lapos;exécution. Cet outil est utilisé depuis des années dans lapos;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 lapos;utiliser pour des études de cas industrielles. La principale raison à cela est la difficulté pour lapos;encoder vers des outils de preuve automatique. Aussi, son utilisation nécessite beaucoup de travail de la part de lapos;utilisateur. Frama-C et WP napos;utilisent donc pas cette logique. Dans un travail récent nous avons décrit comment étendre lapos;outillage de WP pour décrire lapos;empreinte mémoire de structures de données en C. Lapos;idée est dapos;avoir un langage de spécification capable de capturer la majorité de la puissance de la logique de séparation sans avoir à lapos;encoder dans les outils de preuve. Le but de ce postdoc est dapos;expérimenter lapos;usage de ce formalisme pour décrire des cas réels et dapos;implémenter son support au sein de Frama-C et WP.

Profil du candidat : Doctorat en méthodes formelles