This folder contains four models with proofs for different cases of the Responsibility Sensitive Safety model for self-driving cars, for proof-checking Theorems 1-4 of "M. Strauss, S. Mitsch. Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars. In 17th International Conference on Tests and Proofs (TAP 2023), Proceedings, Leicester, UK, Springer, 2023.".

These proofs are executable on KeYmaera X version 5.0.1 https://github.com/LS-Lab/KeYmaeraX-release/releases/tag/5.0.1

Theorem 1: Same direction safety
Theorem 2:  Opposite direction safety 
Theorem 3: Same direction optimality
Theorem 4: Opposite direction optimality