VeriLHyS

VeriLHyS (VERIfying LTL properties of HYbrid Systems) is a tool developed and maintained by the Formal Methods for Systems & Software Design research unit at Fondazione Bruno Kessler.

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.

Latest News