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
A computable and compositional semantics for hybrid automata
Bresolin, D.; Collins, P.; Geretti, L.; Segala, R.; Villa, T.; Zivanovic, S.
23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC ’20), April 22-24, 2020, Sydney, Australia, DOI: 10.1145/ 3365365.3382202
Higher Order Method for Differential Inclusions
Zivanovic, S.; Collins, P.; Geretti, L.; Bresolin, D.; Villa, T.
Journal of Scientific Computing (submitted), 2020, pre-print https://arxiv.org/abs/2001.11330
Model checking dynamical systems
Collins, P.
Nieuw archief voor Wiskunde, Volume 5 / 17, Issue 3, Sep. 2016, pg. 214-220
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
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