Approche algébrique pour la vérification de programmes

Nous désirons étudier la possibilité de faire de l’analyse de programmes en utilisant une approche algébrique. Plus précisément, on s’intéresse au problème de la comparaison de code : aborder ce problème nous permet, entre autres, d’identifier les différences entre deux versions d’un code ou de vérifier si un code optimisé est équivalent à sa version non optimisée. On vise donc à ramener la comparaison de programmes à une simple manipulation algébrique similaire aux manipulations que l’on a l’habitude de faire en algèbre classique. Par ailleurs, outre la comparaison de programmes, l’approche proposée pourrait être utilisée dans d’autres contextes d’analyse de programmes comme, par exemple, la synthèse de programmes ou la vérification par évaluation de modèles (model-checking).

Faculty Supervisor:

M. Béchir Ktari

Student:

François Lajeunesse-Robert

Partner:

Recherche et développement pour la défense Canada (RDDC Valcartier)

Discipline:

Mathematics

Sector:

Information and communications technologies

University:

Université Laval