Neural networks are widely used in numerous applications including safety-critical ones such as control and planning for autonomous systems. A central question is how to verify that they are correct with respect to some specification. Beyond correctness or robustness, we are also interested in questions such as explainability and fairness, that can in turn be specified as formal verification problems. In this course, we will see how formal methods approaches introduced in the context of program verification can be leveraged to address the verification of neural networks.




Drones and robots need to build maps of their environments to plan their motion and navigate. Moreover, enforcing rules and verifying that these moving entities stick to their specifications is essential for safety. This course will focus on safe robot navigation, introduce map building techniques, present motion planning methods and give an introduction to control and verification of the resulting hybrid systems.