Résumé
Dans ce séminaire, Jacques-Henri Jourdan a présenté la logique de séparation Iris. Cette logique, récemment développée avec l'aide de l'assistant de preuve Coq, permet la vérification de programmes concurrents à grain fin en offrant la possibilité de définir des protocoles personnalisés d'interaction entre fils d'exécution ou entre composants logiciels.
Ces protocoles sont définis grâce à deux outils simples et fondamentaux, néanmoins particulièrement puissants : les invariants et l'état fantôme. L'exposé a décrit ces deux concepts et les règles de raisonnement associées, tout en démontrant à l'aide de plusieurs exemples leur puissance et leur flexibilité.
