| Resumé |
L'objet de cette thèse est la logique de séparation asynchrone, une logique de programme pour les langages de programmation concurrents et à mémoire partagée. Le lien entre une preuve d'un programme dans une logique de séparation concurrente et la sémantique de ce programme est exprimée par le théorème de correction de cette logique. Cette thèse introduit deux théorèmes de corrections. Le premier, le théorème de correction asynchrone, exprime dans le langage des jeux de gabarits sur des graphes asynchrones l'absence de courses des programmes bien spécifiés. L'autre étend la logique de séparation concurrente Iris avec un théorème de correction relationnel qui permet d'établir des simulations entre un programme concurrent concret et un modèle abstrait, formalisé comme un système de transition. Une application de ce théorème est la preuve de terminaison de programmes concurrent sous l'hypothèse d'un ordonnanceur équitable. |