Safe and secure systems, such as autonomous vehicles, flight-control systems, medical devices, and biometric authentication systems, are ubiquitous in modern life. A lapse in the safety or security of such systems may lead to catastrophic consequences. Therefore, it is important to formally verify that these systems work correctly.

In this talk, Dr Inzemamul Haque will present some of the mathematical foundations underlying formal verification and illustrate how they arise in three of my research problems: (i) the verification of an operating-system microkernel used in safety- and security-critical settings such as military and avionics platforms; (ii) the synthesis of controllers for dynamical systems using neural networks guided by temporal-logic specifications; and (iii) action planning in collaborative multi-robot systems. The focus of the talk will be on the core ideas behind these approaches, including refinement-based reasoning, logical specification of system behavior, and automated reasoning using SAT and SMT solvers. Through these examples, he will highlight how mathematical logic and algorithmic verification techniques contribute to building safe and trustworthy systems.

All are welcome!