VerSAILLE & Mosaic

Welcome to the teaching materials repository for VerSAILLE and Mosaic. This repository is meant to provide resources for learning about VerSAILLE & Mosaic --- a combination of techniques that admits using the rigorous mathematical foundations of differential dynamic logic ($d\mathcal{L}$) to reason about neural network control systems.

Let us start with some terminology:

• VerSAILLE is the theoretical framework that helps us to come up with correct-by-construction verification properties for Neural Networks deployed in control systems.
• Mosaic is an abstract framework for lifting off-the-shelf Open-Loop Neural Network Verification Tools to the task of verifying polynomial arithmetic specifications of arbitrary propositional structure. The framework preserves a verifier's completeness.
• $\mathbf{N^3V}$ is a concrete implementation of the Mosaic framework for $\mathrm{ReLU}$ neural networks and internally uses nnenum.

Getting Started

1. Please follow the installation instructions
2. After starting the container (see installation instruction), open the following link in your browser:
   http://127.0.0.1:8888/lab?token=versaille
3. This should open a Jupyter Notebook Instance where Intro.ipynb tells you about the next steps.

Note on files in Docker Container:
When called as explained in INSTALLATION.md, Docker will create a volume vdata, i.e. a persistent storage, on your computer which will store all data contained in your Jupyter Lab working directory (/data). This way, when you start the container again (using the same command) your data should still be there (unless you cleaned up your docker installation.)

• To copy data from the docker container to your computer use the following instructions:

  > CID=$(docker run -d -v vdata:/data/ -p 8888:8888 samweb/versaille)
  docker cp $CID:/data/<File I want to copy> ./<where I want to copy it to>

• To change this default behavior, you can use mounts

Literature

To learn more about the topics covered in this repository, there exist various pieces of literature:

• To learn about differential dynamic logic and KeYmaera X:
  • Textbook by André Platzer
  • Short-Form Overview
  • KeYmaera X Tutorial
• To learn about ModelPlex (the monitoring technology that VerSAILLE is built upon):
  • Paper
  • Textbook Chapter
• To learn about VerSAILLE & Mosaic:
  • Paper
  • Slides from SAIV'24

Support

If you struggle with any of the materials offered in this repository, please reach out to Samuel Teuber.