Jobs

Offre de thèse : Vérification formelle de systèmes interactifs par approche déductive

L’objectif de cette thèse est de contribuer à la vérification formelle des propriétés graphiques sur les langages réactifs en développant une approche déductive reposant sur le calcul des plus faibles préconditions. Cet objectif est original car d’une part l’approche vise à adapter aux
langages réactifs une approche de vérification formelle qui est classique dans le domaine des langages impératifs ; et d’autre part elle cherche à vérifier formellement des propriétés
relatives à l’interface homme-machine, particulièrement les propriétés graphiques.

Mots clefs : Logiciels réactifs, Vérification formelle déductive, Plus faible précondition
Lieu : Ecole Nationale de l’Aviation Civile, Toulouse – France
Dates : Candidatures attendues jusqu’au 30/04/2022
Démarrage de la thèse prévu : octobre 2022
Durée : 3 ans