Overt provides a relational piecewise linear over-approximation of any multi-dimensional functions. The over-approximation is useful for verifying systems with non-linear dynamics. In particular, we used Overt for verifying non-linear dynamical systems that are controlled by neural networks.

Output of Overt is a list of equality and inequality constraints that may include non-linear operations like min and max. Overt is guaranteed to identify the tightest linear piecewise over-approximation. In addition, Overt algorithm has a linear complexity, as the function dimension grows.