Current Work

  • Fast and Guaranteed Safe Controller Synthesis - This paper is accepted to the International Conference on Computer-Aided Verification (CAV) 2020. In this paper, we use Lyapunov functions of the tracking error between the actual trajectory and the reference to bound the value of such tracking error. For reference controllers, we use SMT-encoding and SMT solvers to find the piece-wise linear reference trajectories. [BibTex]

Previous Work