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


Parametric formal verification: the robotic paint spraying case study
Geretti, L.; Muradore, R.; Bresolin, D.; Fiorini, P.; Villa, T.;
20th World Congress of the International Federation of Automatic Control (IFAC 2017), 9-14 July 2017, pg. 9658-9663


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

Usage of the library and applications


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


Formal verification of robotic surgery tasks by reachability analysis
Bresolin, D.; Geretti, L.; Muradore, R.; Fiorini, P.; Villa, T.
Microprocessors and Microsystems, Volume 39, Issue 8, November 2015, pg. 836-842, DOI: 10.1016/j.micpro.2015.10.006


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