1: \begin{abstract}

2: 

3: We introduce a counter-example guided inductive synthesis (CEGIS)

4: framework for synthesizing continuous-time switching controllers that

5: guarantee reach while stay (\RWS) properties of the closed loop

6: system. The solution is based on synthesizing control Lyapunov

7: functions (CLFs) for switched systems, that yield switching

8: controllers with a guaranteed minimum dwell time in each mode. Next,

9: we use a CEGIS-based approach to iteratively solve the resulting

10: quantified exists-forall constraints, and find a CLF. We introduce

11: refinements to the CEGIS procedure to guarantee termination, as well

12: as heuristics to increase convergence speed. Finally, we evaluate our

13: approach on a set of benchmarks ranging from two to six state

14: variables, providing a preliminary comparison with related tools.  Our

15: approach shows significant speedups, thus demonstrating the promise of

16: nonlinear SMT solvers for synthesizing provably correct switching

17: control laws.

18: \end{abstract}

19: