Contrats publics et privés pour ACSL

Description de l'offre : Frama-C est une plateforme collaborative de lapos;analyse de programmes écrits en C. Cette plateforme comprend un langage de spécification nommé ACSL basé sur la notion de contrat. Ces contrats, fournis via des annotations dans le code, permettent de spécifier ce que lapos;on attend des différentes fonctions dapos;un programme. Il est ensuite possible de vérifier que le programme est conforme aux différents contrats à lapos;aide des analyseurs de la plateforme. Une limitation actuelle des contrats vis-à-vis du langage C est quapos;ils ne permettent pas facilement de spécifier des contrats différents (interne/privé, externe/public) pour des modules dapos;un système lorsque ceux-ci cachent les détails dapos;implémentation aux modules utilisateurs. Pour cela, une différenciation entre contrat public et contrat privé est nécessaire, mais également les moyens de faire le lien entre les deux pour assurer la cohérence globale de la spécification et de lapos;analyse.

Profil du candidat : Doctorat en vérification de programme ou sémantique des langages de programmation