ARCH-COMP22 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking

Lei Bu; Goran Frehse; Atanu Kundu; Rajarshi Ray; Yuhui Shi; Enea Zaffanella

doi:10.29007/lnzf

ARCH-COMP22 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking

Lei Bu, Goran Frehse, Atanu Kundu, Rajarshi Ray, Yuhui Shi, Enea Zaffanella

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

Abstract

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2022. In this edition, five tools have been applied to solve six different benchmark problems in the category for piecewise constant dynamics: BACH, PHAVer, PHAVerLite, SAT-Reach, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

Original language	English
Pages (from-to)	44-57
Number of pages	14
Journal	EPiC Series in Computing
Volume	90
DOIs	https://doi.org/10.29007/lnzf
Publication status	Published - 1 Jan 2022
Event	9th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2022 - Munich, Germany Duration: 5 Sept 2022 → 5 Sept 2022

Access to Document

10.29007/lnzf

Cite this

@article{daeaf9d4e066460793aa02c5a956f865,

title = "ARCH-COMP22 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking",

abstract = "This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2022. In this edition, five tools have been applied to solve six different benchmark problems in the category for piecewise constant dynamics: BACH, PHAVer, PHAVerLite, SAT-Reach, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.",

author = "Lei Bu and Goran Frehse and Atanu Kundu and Rajarshi Ray and Yuhui Shi and Enea Zaffanella",

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

year = "2022",

month = jan,

day = "1",

doi = "10.29007/lnzf",

language = "English",

volume = "90",

pages = "44--57",

journal = "EPiC Series in Computing",

issn = "2398-7340",

}

TY - JOUR

T1 - ARCH-COMP22 Category Report

T2 - 9th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2022

AU - Bu, Lei

AU - Frehse, Goran

AU - Kundu, Atanu

AU - Ray, Rajarshi

AU - Shi, Yuhui

AU - Zaffanella, Enea

PY - 2022/1/1

Y1 - 2022/1/1

N2 - This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2022. In this edition, five tools have been applied to solve six different benchmark problems in the category for piecewise constant dynamics: BACH, PHAVer, PHAVerLite, SAT-Reach, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

AB - This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2022. In this edition, five tools have been applied to solve six different benchmark problems in the category for piecewise constant dynamics: BACH, PHAVer, PHAVerLite, SAT-Reach, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

U2 - 10.29007/lnzf

DO - 10.29007/lnzf

M3 - Conference article

AN - SCOPUS:85148890195

SN - 2398-7340

VL - 90

SP - 44

EP - 57

JO - EPiC Series in Computing

JF - EPiC Series in Computing

Y2 - 5 September 2022 through 5 September 2022

ER -

ARCH-COMP22 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking

Abstract

Access to Document

Fingerprint

Cite this