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

Luca Geretti; Julien Alexandre dit Sandretto; Matthias Althoff; Luis Benet; Pieter Collins; Marcelo Forets; Elena Ivanova; Yangge Li; Sayan Mitra; Stefan Mitsch; Christian Schilling; Mark Wetzlinger; Daniel Zhuang

doi:10.29007/93f2

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

Luca Geretti
, Julien Alexandre dit Sandretto
, Matthias Althoff
, Luis Benet
, Pieter Collins
, Marcelo Forets
, Elena Ivanova
, Yangge Li
, Sayan Mitra
, Stefan Mitsch
, Christian Schilling
, Mark Wetzlinger
, Daniel Zhuang

University of Southern California
Technical University of Munich
Instituto de Fisica
Universidad Nacional Autónoma de México
Department of Data Science and Knowledge Engineering
Maastricht University
Universidad de la República
University of Illinois at Urbana-Champaign
Carnegie Mellon University
Aalborg University

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

2 Citations (Scopus)

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 2023. This year, 6 tools participated: Ariadne, CORA, DynIbex, JuliaReach, KeYmaera X and Verse (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.

langue originale	Anglais
Pages (de - à)	61-83
Nombre de pages	23
journal	EPiC Series in Computing
Volume	96
Les DOIs	https://doi.org/10.29007/93f2
état	Publié - 1 janv. 2023
Evénement	10th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2023 - San Antonio, États-Unis Durée: 9 mai 2023 → 9 mai 2023

Accès au document

10.29007/93f2

Contient cette citation

@article{36cf4a55cca542b1a2f200023387326e,

title = "ARCH-COMP23 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 2023. This year, 6 tools participated: Ariadne, CORA, DynIbex, JuliaReach, KeYmaera X and Verse (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.",

keywords = "continuous systems, formal methods, hybrid systems, nonlinear dynamics, reachability analysis, verification",

author = "Luca Geretti and \{dit Sandretto\}, \{Julien Alexandre\} and Matthias Althoff and Luis Benet and Pieter Collins and Marcelo Forets and Elena Ivanova and Yangge Li and Sayan Mitra and Stefan Mitsch and Christian Schilling and Mark Wetzlinger and Daniel Zhuang",

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

year = "2023",

month = jan,

day = "1",

doi = "10.29007/93f2",

language = "English",

volume = "96",

pages = "61--83",

journal = "EPiC Series in Computing",

issn = "2398-7340",

publisher = "EasyChair",

}

TY - JOUR

T1 - ARCH-COMP23 Category Report

T2 - 10th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2023

AU - Geretti, Luca

AU - dit Sandretto, Julien Alexandre

AU - Althoff, Matthias

AU - Benet, Luis

AU - Collins, Pieter

AU - Forets, Marcelo

AU - Ivanova, Elena

AU - Li, Yangge

AU - Mitra, Sayan

AU - Mitsch, Stefan

AU - Schilling, Christian

AU - Wetzlinger, Mark

AU - Zhuang, Daniel

PY - 2023/1/1

Y1 - 2023/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 2023. This year, 6 tools participated: Ariadne, CORA, DynIbex, JuliaReach, KeYmaera X and Verse (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.

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 2023. This year, 6 tools participated: Ariadne, CORA, DynIbex, JuliaReach, KeYmaera X and Verse (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.

KW - continuous systems

KW - formal methods

KW - hybrid systems

KW - nonlinear dynamics

KW - reachability analysis

KW - verification

U2 - 10.29007/93f2

DO - 10.29007/93f2

M3 - Conference article

AN - SCOPUS:85192134483

SN - 2398-7340

VL - 96

SP - 61

EP - 83

JO - EPiC Series in Computing

JF - EPiC Series in Computing

Y2 - 9 May 2023 through 9 May 2023

ER -

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

Résumé

Accès au document

Empreinte digitale

Contient cette citation