Fondations algorithmiques pour la certification des systèmes

Cette séance de cours de l'instructeur de Max Planck Institute for Software Systems se concentre sur les défis de la conception de systèmes avec des composants peu fiables. Il couvre des sujets tels que les programmes multithreaded shared-memory, la vérification limitée, l'analyse limitée de k-context et l'utilisation de diagrammes de décision binaires pour une vérification efficace. La séance de cours se penche également sur le caractère décidable de l'accessibilité liée au contexte et sur l'importance de la fermeture à la baisse des langues dans la vérification. En outre, il explore la relation entre la vérification séquentielle et la vérification liée au contexte, ainsi que l'application d'essais randomisés avec des garanties formelles. La séance de cours se termine par des discussions sur la synthèse des contrôleurs pour les systèmes cyberphysiques, la théorie de la confiance dans la conception des systèmes et les considérations éthiques de l'ingénierie de certification parfaite.