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

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 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.

Original language	English
Pages (from-to)	61-83
Number of pages	23
Journal	EPiC Series in Computing
Volume	96
DOIs	https://doi.org/10.29007/93f2
Publication status	Published - 1 Jan 2023
Event	10th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2023 - San Antonio, United States Duration: 9 May 2023 → 9 May 2023

Keywords

continuous systems
formal methods
hybrid systems
nonlinear dynamics
reachability analysis
verification

Access to Document

10.29007/93f2

Cite this

@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",

}

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

Abstract

Keywords

Access to Document

Fingerprint

Cite this