Publications

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


Model checking dynamical systems
Collins, P.
Nieuw archief voor Wiskunde, Volume 5 / 17, Issue 3, Sep. 2016, pg. 214-220


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: 10.1002/RNC.2914


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: 10.3182/20120606-3-NL-3011.00046


Numerical solutions to noisy systems
Zivanovic, S.; Collins, P.
49th IEEE Conference on Decision and Control (CDC), pg. 798–803, Dec 2010, DOI: 10.1109/CDC.2010.5717780

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: 10.1145/3140237


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: 10.1109/JPROC.2015.2453253


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: 10.1109/IWCMC.2011.5982784