Théorèmes de correction asynchrone et relationnelle de la logique de séparation concurrente

The subject of this thesis is concurrent separation logic, a program logic for concurrentshared-memory languages. The relation between the proof of a program in a separationlogic and the semantics of this program is expressed by the soundness theorem ofthis logic. This thesis introduces two soundness theorems. The first, the asynchronoussoundness theorem, expresses the absence of data race in well specified programs inthe language of template games in asynchronous graphs. The second part of this thesisextends the Iris concurrent separation logic with a relational soundness theorem whichallows to establish simulations between a concrete program and an abstract modelexpressed as a state transition system. An application of this theorem is the proof oftermination of concurrent programs under the assumption of a fair scheduler.L’objet de cette thèse est la logique de séparation asynchrone, une logique de pro-gramme pour les langages de programmation concurrents et à mémoire partagée. Lelien entre une preuve d’un programme dans une logique de séparation concurrente etla sémantique de ce programme est exprimée par le théorème de correction de cettelogique. Cette thèse introduit deux théorèmes de corrections. Le premier, le théorèmede correction asynchrone, exprime dans le langage des jeux de gabarits sur des graphesasynchrones l’absence de courses des programmes bien spécifiés. L’autre étend lalogique de séparation concurrente Iris avec un théorème de correction relationnelqui permet d’établir des simulations entre un programme concurrent concret et unmodèle abstrait, formalisé comme un système de transition. Une application de cethéorème est la preuve de terminaison de programmes concurrent sous l’hypothèsed’un ordonnanceur équitable