Summary for README.md

README.md

@@ -1,3 +1,7 @@
+# Overview
+
+This repository is the artifact with a formal model and formal safety proofs for the ABZ'25 case study in differential dynamic logic (dL). The case study considers an autonomous car driving on a highway with a neural network controller avoiding collisions with neighbouring cars. Using KeYmaera X's dL implementation we prove collision-freedom on an infinite time horizon which ensures that safety is preserved independently of trip length. The safety guarantees hold for time-varying reaction time and brake force. Our dL model considers the single lane scenario with cars ahead or behind. We demonstrate dL and its tools are a rigorous foundation for runtime monitoring, shielding, and neural network verification.
+
 # How to run
 
 The docker image can be built directly or downloaded online.
@@ -36,4 +40,4 @@ By default, docker saves the verification results inside the Docker container.
 To move the files to the host, [you need to copy them while the container is still running](https://stackoverflow.com/questions/22049212/copying-files-from-docker-container-to-host).
 
 The repository also contains the previous verification results.  
-These can be inspected as explained [here](versaille/README.md)
+These can be inspected as explained [here](versaille/README.md)