La séparation est tout ce dont vous avez besoin : Fondations pour la vérification modulaire

Cette séance de cours de l'instructeur couvre les fondements de la vérification modulaire de programmes concomitants réalistes utilisant la logique de séparation. Il traite des défis de la convergence, de l'importance d'atteindre la localisation des fils en gardant les fils séparés et de l'application de la logique de séparation pour atteindre cet objectif. La séance de cours explore également les points faibles de la logique de séparation, l'histoire de réussite de la logique de séparation dans les outils de vérification, et la complexité de l'état mutable partagé dans les programmes simultanés. Elle s'inscrit dans les subtilités du comptage des références, des autorisations de fantômes et de la vérification formelle de l'IPC microkernel. La séance de cours se termine par une discussion sur le langage de programmation Rust, son système de type et les défis à relever pour assurer la sécurité dans les programmes Rust.