ARCH-COMP25 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

Luca Geretti; Julien Alexandre Dit Sandretto; Matthias Althoff; Luis Benet; Pieter Collins; Marcelo Forets; Stefan Mitsch; Ismail Patel; Maximilian Perschl; Christian Schilling; Joris Tillet

doi:10.29007/7br2

ARCH-COMP25 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

Luca Geretti
, Julien Alexandre Dit Sandretto
, Matthias Althoff
, Luis Benet
, Pieter Collins
, Marcelo Forets
, Stefan Mitsch
, Ismail Patel
, Maximilian Perschl
, Christian Schilling
, Joris Tillet

University of Verona
Technical University of Munich
Universidad Nacional Autónoma de México
Maastricht University
Universidad de la República
DePaul University
Aalborg University

Research output: Contribution to journal › Conference article › peer-review

Abstract

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 2025. 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 seven benchmark problems, three of them featuring some aspects of 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.

Original language	English
Pages (from-to)	39-70
Number of pages	32
Journal	EPiC Series in Computing
Volume	108
DOIs	https://doi.org/10.29007/7br2
Publication status	Published - 1 Jan 2025
Event	12th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2025 - Virtual, Online Duration: 4 Jun 2025 → 4 Jun 2025

Keywords

formal verification
hybrid systems
nonlinear systems
reachability analysis
theorem proving

Access to Document

10.29007/7br2

Cite this

@article{82fb8a5f745d4b7db198709174459759,

title = "ARCH-COMP25 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics",

abstract = "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 2025. 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 seven benchmark problems, three of them featuring some aspects of 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.",

keywords = "formal verification, hybrid systems, nonlinear systems, reachability analysis, theorem proving",

author = "Luca Geretti and Sandretto, \{Julien Alexandre Dit\} and Matthias Althoff and Luis Benet and Pieter Collins and Marcelo Forets and Stefan Mitsch and Ismail Patel and Maximilian Perschl and Christian Schilling and Joris Tillet",

note = "Publisher Copyright: {\textcopyright} 2025, EasyChair. All rights reserved.; 12th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2025 ; Conference date: 04-06-2025 Through 04-06-2025",

year = "2025",

month = jan,

day = "1",

doi = "10.29007/7br2",

language = "English",

volume = "108",

pages = "39--70",

journal = "EPiC Series in Computing",

issn = "2398-7340",

}

TY - JOUR

T1 - ARCH-COMP25 Category Report

T2 - 12th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2025

AU - Geretti, Luca

AU - Sandretto, Julien Alexandre Dit

AU - Althoff, Matthias

AU - Benet, Luis

AU - Collins, Pieter

AU - Forets, Marcelo

AU - Mitsch, Stefan

AU - Patel, Ismail

AU - Perschl, Maximilian

AU - Schilling, Christian

AU - Tillet, Joris

PY - 2025/1/1

Y1 - 2025/1/1

N2 - 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 2025. 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 seven benchmark problems, three of them featuring some aspects of 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.

AB - 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 2025. 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 seven benchmark problems, three of them featuring some aspects of 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.

KW - formal verification

KW - hybrid systems

KW - nonlinear systems

KW - reachability analysis

KW - theorem proving

UR - https://www.scopus.com/pages/publications/105027181685

U2 - 10.29007/7br2

DO - 10.29007/7br2

M3 - Conference article

AN - SCOPUS:105027181685

SN - 2398-7340

VL - 108

SP - 39

EP - 70

JO - EPiC Series in Computing

JF - EPiC Series in Computing

Y2 - 4 June 2025 through 4 June 2025

ER -

ARCH-COMP25 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this