The project proposes new methods for SMT-based model checking of liveness properties in hybrid systems using discrete abstraction derived from Lyapunov-like certificates and reachability analysis.