Séminaire en ligne, 17 décembre 2020
Pour assister à la rencontre, se rendre sur https://ent-services.ens-lyon.fr/entVisio/ choisir Chocola dans le menu déroulant, mettre son nom comme identifiant, et Bruxelles sans majuscule comme dernier champ. Autoriser les popups, et changer de navigateur au besoin.
15h: accueil et problèmes de connexion 15h15: début de l'exposé 16h15: questions et discussion 17h: adieu et problèmes de déconnexion Merci aux auditeurs de couper micro et caméra (sauf éventuellement, lorsqu'ils souhaitent poser une question). Les questions peuvent aussi être posées dans la fenêtre de chat.
En cas de problème ou de question, écrire à chocola-gestion chez ens-lyon.fr.
Programme
- 15:00 – 17:00
-
Jérémie Koenig (Yale University)Invited talk: Refinement-Based Game Semantics for Certified Components
Current practices ensure software reliability through careful testing, but while testing can reveal the presence of bugs, it cannot entirely guarantee their absence. By contrast, certified systems come with a formal specification and a computer-checked proof of correctness, providing strong evidence that the system behaves as expected in all possible scenarios. Over the past decade, researchers have been able to build certified systems of significant size and complexity, including compilers, processor designs, operating system kernels and more. Building on these successes, the DeepSpec project seeks to assemble them as certified components to build large-scale heterogeneous certified systems. However, by necessity, these certified components use a broad variety of semantic models and verification techniques. To connect them, we must first embed them into a common, general-purpose model. The work I will present proposes to combine game semantics, algebraic effects and the refinement calculus to build models suitable for this task. In particular, certified abstraction layers and the certified compiler CompCert can be embedded into a single framework supporting heterogeneous components, stepwise refinement, and data abstraction.
