ARCH-COMP24 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics
We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2024. This year, 5 tools participated: Ariadne, CORA, DynIbex, JuliaReach and KeYmaera X (in alphabetic order). These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.
Authors
- Matthias Althoff (ORCID: https://orcid.org/0000-0003-3733-842X)
- Marcelo Forets (ORCID: https://orcid.org/0000-0002-9831-7801)
- Pieter Collins (ORCID: https://orcid.org/0000-0002-8896-9603)
- Luis Benet (ORCID: https://orcid.org/0000-0002-8470-9054)
- Stefan Mitsch (ORCID: https://orcid.org/0000-0002-3194-9759)
- Luca Geretti (ORCID: https://orcid.org/0000-0001-6889-0706)
- Christian Schilling (ORCID: https://orcid.org/0000-0003-3658-1065)
- Joris Tillet (ORCID: https://orcid.org/0000-0002-1955-6725)
- Julien Alexandre Dit Sandretto (ORCID: https://orcid.org/0000-0002-6185-2480)
- Mark Wetzlinger (ORCID: https://orcid.org/0000-0002-2794-5077)
Institutions
- University of Verona (IT)
Publication Details
- Journal
- EPiC series in computing
- Published
- 2024-10-10
- DOI
- https://doi.org/10.29007/21ch
- Citations
- 1
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.36
Funders
- European Commission
- Télécom Paris