Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
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.