Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Actualité - Soutenance HDR de Frédéric Dabrowski (5/11/24)

 English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37



Soutenance HDR de Frédéric Dabrowski (5/11/24)

Titre :
Méthodes formelles pour la synchronisation des programmes concurrents et parallèles

Résumé :

Les travaux présentés portent sur l’application des méthodes formelles à la sémantique des langages de programmation concurrente et parallèle. Il s’agit de manière générale de s’assurer que les programmes ont une sémantique bien définie et de vérifier, à priori, qu’ils ne provoqueront pas d’erreur à l’exécution. Dans ce contexte, la bonne synchronisation des différents composants d’un programme est un point essentiel. Nous verrons comment les méthodes formelles peuvent, pour différents types de modèle de programmation concurrente et parallèle, permettre d’atteindre cet objectif. Pour une grande partie des travaux présentés, l’utilisation de l’assistant de preuve Coq permet de renforcer la confiance dans les résultats qui reposent sur des développements mathématiques entièrement vérifiés par ordinateur. Les domaines d’application sont la détection d’erreur de synchronisation pour le langage Java, la formalisation de la notion de bonne synchronisation pour un langage parallèle à base de sections atomiques supportant le parallélisme imbriqué et la vérification de propriétés de bonne formation pour des programmes utilisant la librairie de programmation parallèle BSPlib.