From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes

Jonathan Hellwig, Lukas Schäfer, Long Qian +2

Synthesizing controllers that enforce both safety and actuator constraints is a central challenge in the design of cyber-physical systems. State-of-the-art reachability methods bas…