This lecture by the instructor from Max Planck Institute for Software Systems focuses on the challenges of designing systems with unreliable components. It covers topics such as multithreaded shared-memory programs, bounded verification, k-context bounded analysis, and the use of binary decision diagrams for efficient verification. The lecture also delves into the decidable nature of context-bounded reachability and the importance of downward closures of languages in verification. Furthermore, it explores the relationship between sequential verification and context-bounded verification, as well as the application of randomized testing with formal guarantees. The lecture concludes with discussions on controller synthesis for cyber-physical systems, the theory of trust in systems design, and the ethical considerations of perfect certification engineering.
This video is available exclusively on Mediaspace for a restricted audience. Please log in to MediaSpace to access it if you have the necessary permissions.
Watch on Mediaspace