Bibliothèques écrites en Isabelle

Spécification et preuves seL4.

Projet cohérent.

Un outil de génération automatique de preuves de correction Isabelle/HOL pour les protocoles de sécurité.

Une définition formelle et une vérification du système F. À étendre au système Fc.

Mise en œuvre à haute assurance de la famille de protocoles Ouroboros.