Friendly Competition

Call for Participation

ARCH-COMP 2021
5th International Competition on Verifying Continuous and Hybrid Systems

Call for Participation

1. Join a group that treats problems similar to yours (by March 31).
- Piecewise Constant Dynamics
- Piecewise Affine Dynamics
- Nonlinear Dynamics
- Bounded model checking
- Falsification
- Stochastic Models
- Hybrid Programs
- AI Models

2. Each group determines a set of problems and submits preliminary results (by April 30).
- Everybody can propose, all should approve.
- Benchmarks from ARCH repository are preferred.
- Problems are revised in group discussions.
- Send in models and data used to run your tool.

3. Each group prepares a report on the results (by May 31).
- Evaluation chair signals approved results.

4. Each group submits packages for the repeatability evaluation (by June 14)
- Packages have to be submitted here.
- Instructions for upload can be found here.

5. Reports are presented (early July)
- presentation at ARCH workshop, part of IFAC World Congress in Berlin, Germany.
(participants of the competition are not required to attend the workshop)
- published online in EPiC proceedings (indexed by DBLP).

Join by email to:
arch21@easychair.org

General Chairs:
Goran Frehse, ENSTA, IP Paris
Matthias Althoff, Technical University of Munich

Publicity Chair:
Sergiy Bogomolov, Newcastle University

Evaluation Chair:
Taylor T. Johnson, Vanderbilt University

Competition Statutes

The statutes and some tips and tricks are available here.

Results

The competition reports of each year can be found in the corresponding proceedings:

ARCH proceedings 2020

ARCH proceedings 2019

ARCH proceedings 2018

ARCH proceedings 2017

Repeatability Packages

Repeatability packages of all years can be found here.

Participants

Piecewise Constant Dynamics (lead: Goran Frehse); updated January 2021

  • BACH (Lei Bu)
  • PHAVer/SX (Goran Frehse)
  • PHAVerLite (Enea Zaffanella)
  • TROPICAL (Muhammad Syifa'ul Mufid, Dieky Adzkiya, Alessandro Abate)
  • XSpeed (Rajarshi Ray)

Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff); updated January 2021

  • C2E2 (Yangge Li, Chuchu Fan, Sayan Mitra)
  • CORA (Nikolas Kochdumper, Mark Wetzlinger, Matthias Althoff)
  • HyDRA (Stefan Schupp)
  • Hylaa (Stanley Bak)
  • Hylaa-Continuous (Stanley Bak)
  • JuliaReach (Marcelo Forets, Christian Schilling, Daniel Freire)
  • SpaceEx (Goran Frehse)
  • XSpeed (Rajarshi Ray)

Nonlinear Dynamics (lead: Luca Geretti); updated January 2021

  • Ariadne (Luca Geretti, Pieter Collins)
  • CORA (Niklas Kochdumper, Mark Wetzlinger, Matthias Althoff)
  • DynIbex (Alexandre Chapoutot, Julien Alexandre dit Sandretto)
  • Flow* (Xin Chen)
  • Isabelle/HOL (Fabian Immler)
  • JuliaReach (Marcelo Forets, Christian Schilling, David P. Sanders, Luis Benet, Daniel Freire)

Artificial Intelligence and Neural Network Control Systems (AINNCS) (lead: Taylor Johnson); updated January 2021

  • NNV (Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Weiming Xiang, and Taylor T. Johnson)
  • OVERT (Amir Maleki, Chelsea Sidrane)
  • ReachNN* (Jiameng Fan, Qi Zhu, Chao Huang, Wenchao Li)
  • VenMAS (Elena Botoeva, Francesco Leofante)

Stochastic Models (lead: Alessandro Abate); updated January 2021

  • AMYTISS (Abolfazl Lavaei, Mahmoud Khaled, Sadegh Soudjani, and Majid Zamani)
  • FAUST^2 (Arnd Hartmanns)
  • hpnmg (Carina Pilch and Anne Remke)
  • HYPEG (Carina Pilch, Anne Remke)
  • Mascot-SDS (Fedor Shmarov and Sadegh Soudjani)
  • Modest Toolset (ArndHartmanns)
  • ProbReach (Fedor Shmarov and Paolo Zuliani)
  • SReachTools (Abraham Vinod)
  • StocHy (Nathalie Cauchi and Alessandro Abate)

Falsification (lead: Gidon Ernst); updated January 2021

  • ARIsTEO (Claudio Menghi)
  • Breach (Alexandre Donze)
  • falsify (Yoriyuki Yamagata)
  • FalStar (Gidon Ernst, Sean Sedwards, Zhenya Zhang, Paolo Arcaini)
  • S-TaLiRo (Georgios Fainekos, Shakiba Yaghoubi, Logan Mathesen, Giulia Pedrielli)
  • zlscheck (Marc Pouzet, Goran Frehse, Ismail Bennani)

Hybrid Programs (lead: Stefan Mitsch); updated January 2021

  • HHL Prover (Xiangyu Jin, Shuling Wang, Bohua Zhan, Naijun Zhan)
  • Isabelle/HOL/Hybrid-Systems-VCs (Jonathan Julian Huerta y Munive)
  • KeYmaera 3 (Andre Platzer)
  • KeYmaera X (Stefan Mitsch, Andre Platzer, Andrew Sogokon, Yong Kiam Tan)