Séance de cours
Cette séance de cours introduit Dafny, un langage compilé conçu pour la vérification formelle, assurant une exécution correcte du code sans erreurs d'exécution. Il couvre la modélisation de la concurrence, les règles de sécurité, les propriétés de la vivacité et les concepts de mémoire transactionnelle. L'instructeur présente des exemples et des documents sur la concordance et la mémoire transactionnelle, mettant l'accent sur la vérification formelle et la création avancée d'algorithmes.