Verification and Synthesis of Autonomous Systems

This course will provide different techniques on the verification of autonomous systems against stability, regular, or omega-regular properties. Such techniques include Lyapunov theories, reachability analysis, barrier certificates, and model checking. Finally, it will introduce several techniques on designing controllers enforcing properties of interest over the original autonomous systems. This course can be taken for academic credit as part of CU Boulder’s Masters of Science in Computer Scie

• Analyze stability properties of linear systems
• Compute over-approximations of reachable sets
• Perform model checking for finite systems
• Synthesize controllers for safety and reachability

• Basic knowledge of linear systems and algorithms