Below we provide a selection of publications where the theoretical framework and the algorithmic implementation of Ariadne are explained. Additionally, we present some publications where either the relevant applications of the library are discussed, or where the library has been successfully applied to verify systems of industry relevance.
The following papers are provided in descending order of publication and represent the latest developments on a given research direction. For each item, a link to the .pdf file () and a link to the .bib file () is available.
Theory and implementation
Assume-guarantee verification of nonlinear hybrid systems with Ariadne
Benvenuti, L; Bresolin, D.; Collins, P.; Ferrari, A.; Geretti, L.; Villa, T.
International Journal of Robust and Nonlinear Control, Volume 24, Issue 4, Mar. 2014, pg. 699-724, ISSN: 1049-8923, DOI:
Computing the evolution of hybrid systems using rigorous function calculus
Collins, P.; Bresolin, D.; Geretti, L.; Villa, T.
4th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS’12), June 2012, pg. 284-290, DOI:
Usage of the library and applications
Formal Verification of Medical CPS: a Laser Incision Case Study
Geraldes, A.; Geretti, L.; Bresolin, D.; Muradore, R.; Fiorini, P.; Mattos, L.M.; Villa, T.
ACM Transactions on Cyber-Physical Systems, Volume 2, Issue 4, September 2018, 35:1-35:29, DOI:
A platform-based design methodology with contracts and related tools for the design of cyber-physical systems
Nuzzo, P.; Sangiovanni-Vincentelli, A.L.; Bresolin, D.; Geretti, L.; Villa, T.
Proceedings of the IEEE, Volume 103, Issue 11, 2015, pg. 2104-2132, DOI:
Correct-by-construction code generation from hybrid automata specification
Bresolin, D.; Di Guglielmo, L.; Geretti, L.; Villa, T.
Proc. Of the 7th International Wireless Communication and Mobile Computing Conference (IWCMC’11), Jul. 2011, pg. 1660-1665, Print ISBN: 978-1-4244-9539-9, DOI: