About

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 C++ and it is distributed using Git on BitBucket under the GPLv3 license. The release-1.0 repository currently holds the stable version of the library. The development repository introduces a lot of improvements to the code base, it is usable but it is still considered not stable. In addition, verification routines are not currently implemented in the development version. The user interface of the library currently relies on using C++ code directly. Python bindings are available in the development version, but they are mainly focused on low-level routines for numerical analysis. Ariadne is actively supported on both Ubuntu derivatives and macOS.

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.