DSN tutorial

code/nnv/examples/Tutorial/readme.md

@@ -1,6 +1,10 @@
-# Verification and Validation of Neural Networks in Automated Vehicles (NNV Tutorial) - E2023 IEEE IAVVC
+# Safe, Secure, and Trustworthy Artificial Intelligence (AI) via Formal Verification of Neural Networks and Autonomous Cyber-Physical Systems (CPS) - NNV Tutorial at DSN 2024
+
+Previous tutorials at
+
+ - 2023 IEEE IAVVC
+ - EMSOFT'23 (Embedded Systems Week 2023)
 
-Previous tutorial at EMSOFT'23 (Embedded Systems Week 2023)
 
 ## Getting Started
 We recommend using MATLAB Online (**prior license not required!**) to participate in this tutorial, but one can also use a local installation of MATLAB and NNV to follow along as well.
@@ -9,8 +13,7 @@ It is important that participants complete this section before arriving at the t
 
 #### MATLAB Online Instructions
 
-Registered participants should have received a link with a MATLAB license to use in this tutorial. If a participant has not received it, 
-please contact the organizers. 
+Registered participants should have received a link with a MATLAB license to use in this tutorial. If a participant has not received it, please contact the organizers. 
 
 ###### Note: this license is not required if participants already have a valid license for all the toolboxes listed in [installation instructions](/README.md#installation).
 
@@ -27,8 +30,7 @@ To run NNV locally, please follow these [instructions](/README.md#installation).
 
 ## Interactive Tutorial
 
-During this tutorial, one will learn how to represent convex sets as Star sets, load neural networks into NNV, 
-compute reachability analysis of classification neural networks, compute the certified robustness of neural networks and more!
+During this tutorial, one will learn how to represent convex sets as Star sets, load neural networks into NNV, compute reachability analysis of classification neural networks, compute the certified robustness of neural networks, and more!
 
 _Setup_
 
@@ -40,24 +42,24 @@ Open [MATLAB Online](https://workshop-matlab.mathworks.com/) (or MATLAB), then g
 #### Neural Networks (NN)
 
 * Robustness verification on the MNIST dataset.
-    * [Robustness verification of a single image](code/nnv/examples/Tutorial/NN/MNIST/verify_fc.m) using a [model with fully-connected and ReLU layers](code/nnv/examples/Tutorial/NN/MNIST/training_fc.m).
-    * [Robustness verification of a single image](code/nnv/examples/Tutorial/NN/MNIST/verify.m) using a [model with Convolutional, Pooling, Batch Normalization, ReLU, and fully-connected layers](code/nnv/examples/Tutorial/NN/MNIST/training.m)
-    * [Certified robustness](code/nnv/examples/Tutorial/NN/MNIST/verify_fc_allTest.m) of a neural network classifier using a [model with fully-connected and ReLU layers](code/nnv/examples/Tutorial/NN/MNIST/training_fc.m).
+    * [Robustness verification of a single image](NN/MNIST/verify_fc.m) using a [model with fully-connected and ReLU layers](NN/MNIST/training_fc.m).
+    * [Robustness verification of a single image](NN/MNIST/verify.m) using a [model with Convolutional, Pooling, Batch Normalization, ReLU, and fully-connected layers](NN/MNIST/training.m)
+    * [Certified robustness](NN/MNIST/verify_fc_allTest.m) of a neural network classifier using a [model with fully-connected and ReLU layers](NN/MNIST/training_fc.m).
 
 * Robustness verification on the GTSRB dataset.
-    * Includes [training](code/nnv/examples/Tutorial/NN/GTSRB/train.m) and [verification](code/nnv/examples/Tutorial/NN/GTSRB/verify_robust_27.m) scripts as well.
-* Comparison of exact (sound and complete) and approximate (sound and incomplete) methods using Star sets [exact vs approx](code/nnv/examples/Tutorial/NN/compareReachability/reach_exact_vs_approx.m)
+    * Includes [training](NN/GTSRB/train.m) and [verification](NN/GTSRB/verify_robust_27.m) scripts as well.
+* Comparison of exact (sound and complete) and approximate (sound and incomplete) methods using Star sets [exact vs approx](NN/compareReachability/reach_exact_vs_approx.m)
 
 #### Neural Network Control Systems (NNCS)
 
-* Reachability analysis of an [inverted pendulum](code/nnv/examples/Tutorial/NNCS/InvertedPendulum/reach_invP.m).
+* Reachability analysis of an [inverted pendulum](NNCS/InvertedPendulum/reach_invP.m).
 * Safety verification example of an Adaptive Cruise Control (ACC) system.
-    * [Training](code/nnv/examples/Tutorial/NNCS/ACC/Training%20and%20testing). This requires installing Simulink.
-    * [Safety Verification](code/nnv/examples/Tutorial/NNCS/ACC/Verification/verify.m).
-* Safety verification of an Automated Emergency Braking System ([AEBS](code/nnv/examples/Tutorial/NNCS/AEBS))
+    * [Training](NNCS/ACC/Training%20and%20testing). This requires installing Simulink.
+    * [Safety Verification](NNCS/ACC/Verification/verify.m).
+* Safety verification of an Automated Emergency Braking System ([AEBS](NNCS/AEBS))
     * This system contains several neural networks, so a custom control loop is included in the verification script.
 
 In addition, we have also prepared a set of exercises for the participants:
-* Verification of ACAS Xu neural network with ONNX and VNNLIB files: [ONNX & VNNLIB exercise](code/nnv/examples/Tutorial/NN/ACAS%20Xu/exercise_vnnlib_onnx.m)
-* Robustness verification of a neural network: [NN exercise](code/nnv/examples/Tutorial/NN/GTSRB/exercise_verify_robustness.m))
-* Safety verification of a linearized plant model of an adaptive cruise control system: [NNCS exercise](code/nnv/examples/Tutorial/NNCS/ACC/Exercise/exercise_reachability_nncs.m)
+* Verification of ACAS Xu neural network with ONNX and VNNLIB files: [ONNX & VNNLIB exercise](NN/ACAS%20Xu/exercise_vnnlib_onnx.m)
+* Robustness verification of a neural network: [NN exercise](NN/GTSRB/exercise_verify_robustness.m))
+* Safety verification of a linearized plant model of an adaptive cruise control system: [NNCS exercise](NNCS/ACC/Exercise/exercise_reachability_nncs.m)