Ariadne is a library for formal verification of cyber physical systems. In particular, it allows to model such systems as hybrid systems, focusing on nonlinear behavior.
Since the evolution of a nonlinear hybrid system cannot be calculated exactly, Ariadne uses numerical analysis to compute such evolution in an approximate way. The library uses a conservative rounding approach along with rigorous semantics to guarantee the correctness of the results, independently of the numerical precision of the processing machine. In particular, it is able to calculate approximations of the trajectory from above or from below, which allows to prove or disprove properties of the system, respectively.
The library is written in modern C++, with an additional Python 3 interface covering all the most relevant C++ API routines. It is distributed using Git on GitHub under the GPLv3 license. Ariadne is actively supported on both Ubuntu derivatives and macOS, with pre-built packages available.
Ariadne is mainly developed as a collaboration between the University of Verona, Italy and the University of Maastricht, The Netherlands. Given the open nature of the library, we encourage anyone interested in contributing to contact us.
While this website represents the main resource for the documentation of the library, we also maintain a ResearchGate project where the news from this site are backlinked.