Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Méthode formelle (informatique)

Séances de cours associées (29)

Architectures et logiciels fiables Connectez-vous à Mediaspace pour regarder cette vidéo

Explore les architectures fiables, la détection des erreurs, les structures tolérantes aux pannes et la fiabilité des logiciels à travers des exemples tels que la défaillance du missile Patriot et le double contrôleur ABB.

Test basé sur la propriété: QuickChick Connectez-vous à Mediaspace pour regarder cette vidéo

Explore les tests basés sur des propriétés en utilisant QuickChick, en mettant l'accent sur l'exactitude des logiciels, les spécifications et le contrôle dynamique du flux d'information.

Conception de systèmes en réseau performants Connectez-vous à Mediaspace pour regarder cette vidéo

Explore la conception de systèmes en réseau pour des performances robustes, en mettant l'accent sur les applications en temps réel et la vérification formelle.

Encodeur et décoder pour les codes sans préfixe Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre la mise en œuvre et la vérification de l'encodeur et du décodeur pour les codes sans préfixe, y compris les classes et les types, les lemmas sur les arbres, et le théorème principal.

Machines à états finis (FSM)Connectez-vous à Mediaspace pour regarder cette vidéo

Explore les machines d'état fini (FSM) dans la conception de systèmes numériques, couvrant les FSM Mealy et Moore, les diagrammes d'état, l'implémentation VHDL et l'encodage d'état.

Concevoir des systèmes d'intervalles officiellement corrects Connectez-vous à Mediaspace pour regarder cette vidéo

Explore la conception de systèmes intermittents formellement corrects pour les plates-formes de calcul de bord extrême, mettant l'accent sur la justesse, la fiabilité et la sécurité.

Demande de priorité purement fonctionnelle Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre les files d'attente prioritaires purement fonctionnelles, l'implémentation Scala, l'intégration Inoxydable, les propriétés d'exploitation et les files d'attente binomiales.

Concurrence et mémoire transactionnelle en Dafny Connectez-vous à Mediaspace pour regarder cette vidéo

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é.

La séparation est tout ce dont vous avez besoin : Fondations pour la vérification modulaire Connectez-vous à Mediaspace pour regarder cette vidéo

Explore les fondements de la vérification modulaire en utilisant la logique de séparation pour des programmes concomitants réalistes et discute des défis de l'état mutable partagé dans la concorde.