Couvre les bases de Dafny, la concurrence de modélisation et la mise en œuvre de la mémoire transactionnelle avec des preuves de sécurité et de vivacité.
Explore l'importance et les défis des transactions, en mettant l'accent sur les propriétés ACID et les implications pratiques de l'utilisation de la mémoire transactionnelle pour le contrôle de la concurrence.
Couvre les bases des opérations atomiques dans la proximité et le parallélisme, y compris les opérations fournies par le matériel et les algorithmes synchronisés.
