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

Résultats de recherche: Contribution à un journal › Article de conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
Pages (de - à)	39-70
Nombre de pages	32
journal	EPiC Series in Computing
Volume	108
Les DOIs	https://doi.org/10.29007/7br2
état	Publié - 1 janv. 2025
Evénement	12th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2025 - Virtual, Online Durée: 4 juin 2025 → 4 juin 2025

Accès au document

10.29007/7br2

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

@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

Résumé

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation