Adaptive Shielding via Parametric Safety Proofs

How can we keep cyber-physical systems safe in unknown, changing environments? Our latest work empowers engineers to build safety monitors that become increasingly permissive as knowledge about the world is gathered at runtime. Such monitors can be automatically extracted from parametric safety proofs verified with KeYmaera X, leveraging minimal amounts of expert knowledge to offer an unprecedented combination of rigor, modelling flexibility and runtime efficiency.