sentence1: we verify the acceleration and orientation choices as modeled in model 1 above are safe , using a formal proof calculus for dl .
sentence2: we verify the safety of the control algorithm modeled as a hybrid program in model 2 , using a formal proof calculus for dl .