Efficiency Analysis of Formally Verified Adaptive Cruise Controllers

Sarah M. Loos         David Witmer         Peter Steenkiste         Andre Platzer


A webstart version of KeYmaera can be launched here.

The model for the Adaptive Cruise Controller can be downloaded here.
The proof file for the Adaptive Cruise Controller can be downloaded here.
Each of the above files can be loaded into KeYmaera.