Skip to content

Commit

Permalink
Fix paths in tutorial readme, prepare for DSN 2024
Browse files Browse the repository at this point in the history
  • Loading branch information
mldiego authored Jun 12, 2024
1 parent 388483d commit 05faccb
Showing 1 changed file with 20 additions and 18 deletions.
38 changes: 20 additions & 18 deletions code/nnv/examples/Tutorial/readme.md
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -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).

Expand All @@ -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_

Expand All @@ -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)

0 comments on commit 05faccb

Please sign in to comment.