Vérification des programmes avec l'inox : un exemple étendu

Cette séance de cours couvre la vérification des programmes utilisant l'inox, en mettant l'accent sur un exemple étendu lié au format d'image tout à fait OK (QOI). La séance de cours commence par une introduction à QOI, un format de compression d'image sans perte offrant des accélérations significatives. Il se décline ensuite dans l'implémentation de Scala QOI, montrant comment Stainless peut traduire Scala en C. La séance de cours traite également des méthodes d'encodage, des fonctions partielles inverses et du processus de vérification. Les participants sont encouragés à essayer le script de vérification fourni dans le dépôt et à explorer la version entièrement vérifiée pour une compréhension plus approfondie du sujet.