Prerequisite: ENEE460, or students who have taken courses with comparable content may contact the Department. Introduction to formal verification and control synthesis techniques for finite transition systems. Application to continuous and hybrid systems by means of abstractions. Recent developments in control synthesis based on optimization and barrier function techniques.