Overview

Welcome to the Vehicle Tutorial! In this tutorial, you will learn about neural network verification with Vehicle. Vehicle’s installation instructions and user guide are available here. This tutorial was created by:

• Matthew Daggitt
• Wen Kokke
• Ekaterina Komendantskaya
• Bob Atkey
• Luca Arnaboldi
• Natalia Slusarz
• Marco Casadio
• Ben Coke
• Jeonghyeon Lee

If you have any questions about the Vehicle Tutorial, you are invited to join our Slack for questions and discussions.

We hope you enjoy this tutorial!

Table of contents

1. Introduction
2. Getting Started with the Vehicle Specification Language
3. Proving Neural Network Robustness
4. Property-Driven Training
5. Exporting to Agda

Courses taught using the Vehicle Tutorial

This tutorial has been run live and adapted for different audiences at:

• FOMLAS’23 the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems co-allocated with CAV’23 in Paris, France; 18 July 2023;

• VETSS Summer School at the University of Surrey, UK; 23 August 2023; Youtube recording available;

• ICFP’23 the International Conference on Functional Programming in Seattle, USA; 08 September 2023.

We thank all our readers and attendees for their feedback and contribution. This FOMLAS’23 tutorial outline gives a summary of all tutorial resorces.

Citing the Vehicle Tutorial

To cite Vehicle tutorial, please use:

@inproceedings{FoMLAS2023:Vehicle_Tutorial_Neural_Network,
  author    = {
    Matthew Daggitt and Wen Kokke
    and Ekaterina Komendantskaya and Robert Atkey
    and Luca Arnaboldi and Natalia Slusarz
    and Marco Casadio and Ben Coke
    and Jeonghyeon Lee
  },
  title     = {
    The Vehicle Tutorial:
    Neural Network Verification with Vehicle},
  booktitle = {
    Proceedings of the 6th Workshop on
    Formal Methods for ML-Enabled Autonomous Systems},
  editor    = {
    Nina Narodytska and Guy Amir and Guy Katz and Omri Isac},
  series    = {Kalpa Publications in Computing},
  volume    = {16},
  pages     = {1--5},
  year      = {2023},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2515-1762},
  url       = {https://easychair.org/publications/paper/Rkrv},
  doi       = {10.29007/5s2x}
}