VeriLHyS

VeriLHyS enables the specification and automated verification of LTL properties for hybrid automata. It is implemented by integrating several existing tools: CORA for reachability analysis, nuxmv for symbolic model checking, numerical solvers (YALMIP, Mosek) for synthesis of candidate certificate functions, and SMT solvers for certificate validation and abstraction synthesis.

The tool supports both linear and nonlinear (polynomial) dynamics and scales to systems with large discrete structures and complex behaviors.

Website