Course Description:

Complex software systems are everywhere. How do we reason about the correctness of software programs, from distributed message-passing programs to shared-memory concurrent programs to autonomous cyber-physical systems? The area of formal verification provides you with tools that allow you to express the correctness of software programs in a mathematically precise fashion and algorithms that can check for correctness, often with minimal human intervention or input. This course will provide you with the necessary background to reason about topics such as correctness of sequential and concurrent programs, safety of autonomous cyber-physical systems including those that use AI, and core ideas from requirement formalisms based on temporal logic and automata theory. We will examine the theory and algorithms for formal verification in discrete software programs as well as hybrid and nonlinear continuous dynamical systems. This course is meant to be a depth course that focuses on the theoretical considerations for concurrent/distributed programs, timed and probabilistic systems, and hybrid and nonlinear dynamical systems.