Showing eess.SYShow all
3 papers · 1 filter
eess.SY2025
Formal Verification of Control Lyapunov-Barrier Functions for Safe Stabilization with Bounded Controls
Jun Liu
We present verifiable conditions for synthesizing a single smooth Lyapunov function that certifies both asymptotic stability and safety under bounded controls. These sufficient con…
eess.SY2025
Computing Control Lyapunov-Barrier Functions: Softmax Relaxation and Smooth Patching with Formal Guarantees
Jun Liu, Maxwell Fitzsimmons
We present a computational framework for synthesizing a single smooth Lyapunov function that certifies both asymptotic stability and safety. We show that the existence of a strictl…
eess.SY2025
Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions
Jun Liu, Maxwell Fitzsimmons
We investigate the formal synthesis of global polynomial Lyapunov functions for polynomial vector fields. We establish that a sign-definite polynomial must satisfy specific algebra…