Algorithmic Foundations for Systems Certification

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.