ARCH-COMP20 category report: Continuous and hybrid systems with nonlinear dynamics

Luca Geretti; Julien Alexandre Dit Sandretto; Matthias Althoff; Luis Benet; Alexandre Chapoutot; Xin Chen; Pieter Collins; Marcelo Forets; Daniel Freire; Fabian Immler; Niklas Kochdumper; David P. Sanders; Christian Schilling

doi:10.29007/zkf6

ARCH-COMP20 category report: Continuous and hybrid systems with nonlinear dynamics

Luca Geretti
, Julien Alexandre Dit Sandretto
, Matthias Althoff
, Luis Benet
, Alexandre Chapoutot
, Xin Chen
, Pieter Collins
, Marcelo Forets
, Daniel Freire
, Fabian Immler
, Niklas Kochdumper
, David P. Sanders
, Christian Schilling

Informatics 6 - Associate Professorship of Cyber Physical Systems

University of Verona
ENSTA Paris
Universidad Nacional Autónoma de México
University of Dayton
University of Maastricht
Universidad de la República
Carnegie Mellon University
Technical University of Munich
Massachusetts Institute of Technology
Institute of Science and Technology Austria (ISTA)

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

15 Scopus citations

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 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. 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)	49-75
Number of pages	27
Journal	EPiC Series in Computing
Volume	74
DOIs	https://doi.org/10.29007/zkf6
State	Published - 2020
Event	7th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2020 - Virual, Online Duration: 12 Jul 2020 → 12 Jul 2020

Access to Document

10.29007/zkf6

Cite this

@article{af3333254cdc40ed8ddf86204da0f21d,

title = "ARCH-COMP20 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 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. 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.",

author = "Luca Geretti and \{Dit Sandretto\}, \{Julien Alexandre\} and Matthias Althoff and Luis Benet and Alexandre Chapoutot and Xin Chen and Pieter Collins and Marcelo Forets and Daniel Freire and Fabian Immler and Niklas Kochdumper and Sanders, \{David P.\} and Christian Schilling",

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

year = "2020",

doi = "10.29007/zkf6",

language = "English",

volume = "74",

pages = "49--75",

journal = "EPiC Series in Computing",

issn = "2398-7340",

publisher = "EasyChair",

}

TY - JOUR

T1 - ARCH-COMP20 category report

T2 - 7th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2020

AU - Geretti, Luca

AU - Dit Sandretto, Julien Alexandre

AU - Althoff, Matthias

AU - Benet, Luis

AU - Chapoutot, Alexandre

AU - Chen, Xin

AU - Collins, Pieter

AU - Forets, Marcelo

AU - Freire, Daniel

AU - Immler, Fabian

AU - Kochdumper, Niklas

AU - Sanders, David P.

AU - Schilling, Christian

PY - 2020

Y1 - 2020

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 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. 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 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. 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.

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

U2 - 10.29007/zkf6

DO - 10.29007/zkf6

M3 - Conference article

AN - SCOPUS:85105861287

SN - 2398-7340

VL - 74

SP - 49

EP - 75

JO - EPiC Series in Computing

JF - EPiC Series in Computing

Y2 - 12 July 2020 through 12 July 2020

ER -

ARCH-COMP20 category report: Continuous and hybrid systems with nonlinear dynamics

Abstract

Access to Document

Other files and links

Fingerprint

Cite this