Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
En libre accès, dans la limite des places disponibles
-

Résumé

Le quatrième séminaire a approfondi la mécanisation d’une logique de séparation, sujet que le quatrième cours avait juste effleuré. Le conférencier a montré comment construire une telle logique en Coq à partir d’une sémantique naturelle pour un petit langage de type « mini-ML », c’est-à-dire un langage fonctionnel étendu avec des références mutables. Il a ensuite décrit plusieurs outils, toujours intégrés dans Coq, qui facilitent les vérifications de programmes : un calcul de plus faible précondition, des prédicats d’encodage de structures de données, et des tactiques Coq. Tous ces éléments se retrouvent dans son outil CFML de vérification de programmes impératifs.

Intervenant(s)

Arthur Charguéraud