Vérification formelle en Coq de la chaîne des sémantiques pour la compilation d'Esterel

Le sixième et dernier cours, inversé, commencera par le séminaire de Lionel Rieg sur son travail effectué au Collège de France en 2014-2016 sur la vérification formelle des théories d’Esterel. L’exposé présentera d’abord des preuves en Coq des théorèmes de correspondance reliant les différentes sémantiques de plus en plus précises d’Esterel, telles qu’énoncées dans le livre Web “The Constructive Semantics of Esterel” puis affinées dans la thèse d’Olivier Tardieu en 2004 : sémantique logique, sémantique constructive, sémantique par transition de marquages d’états dans les termes. Il introduira ensuite une nouvelle sémantique opérationnelle réalisant la sémantique constructive par propagation dans le programme de jetons colorés, intuitivement proche de la traduction en circuits mais plus facile à traiter. La preuve de cette nouvelle sémantique est actuellement limitée aux programmes sans boucle : elle devra être étendue aux programmes généraux en incorporant un des traitements de la réincarnation présentés dans le cours du 14 mars.