Friendly Competition

Call for Participation

ARCH-COMP 2020
4th International Competition on Verifying Continuous and Hybrid Systems

Call for Participation

1. Join a group that treats problems similar to yours (by April 19).
- 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 May 10).
- 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 (July 12)
- 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:
arch20@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 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 April 2020

  • BACH (Lei Bu)
  • HyCOMP (Sergio Mover, Stefano Tonetta, Alberto Griggio, Alessandro Cimatti)
  • Lyse (Mirco Giacobbe)
  • PHAVer/SX (Goran Frehse)
  • PHAVerLite (Enea Zaffanella)
  • VeriSiMPL (Alessandro Abate, Dieky Adzkiya, Muhammad Syifa'Ul Mufid)

Continuous and Hybrid Systems with Linear Dynamics (lead: Matthias Althoff); updated April 2020

  • C2E2 (Yangge Li, Chuchu Fan, Sayan Mitra)
  • CORA (Nikolas Kochdumper, Mark Wetzlinger, Matthias Althoff)
  • CORA/SX (Goran Frehse)
  • 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 April 2020

  • 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) (new in 2019, lead: Taylor Johnson); updated April 2020

  • JuliaReach (Marcelo Forets, Sebastian Guadalupe, Christian Schilling)
  • nnenum (Stanley Bak)
  • 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)
  • Sherlock (Sriram Sankaranarayanan, Souradeep Dutta, Susmit Jha, and Ashish Tiwari)
  • Verisig (Radoslav Ivanov, James Weimer, Insup Lee)

Stochastic Models (lead: Alessandro Abate); updated April 2020

  • epsilon-delta Abstraction (Sofie Haesaert; TU Eindhoven)
  • FAUST^2 (Sofie Haesaert; Eindhoven University of Technology)
  • HYPEG (Carina Pilch, Anne Remke; University of Muenster)
  • LyapMMC (Mahmoud Salamati, Sadegh Soudjani; Max Planck Institute, University of Newcastle)
  • Modest Toolset (Ernst Moritz Hahn; University of Liverpool)
  • SDCPN (Henk Blom, Hao Ma; Delft University of Technology)
  • SReachTools (Abraham Vinod; University of New Mexico)
  • StocHy (Nathalie Cauchi, Alessandro Abate; University of Oxford)

Bounded Model Checking (lead: Lei Bu); updated April 2020

  • BACH (Lei Bu)
  • HyDRA (Stefan Schupp)
  • TROPICAL (Muhammad Syifa'ul Mufid)
  • XSpeed (Rajarshi Ray)

Falsification (lead: Gidon Ernst); updated April 2020

  • 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 April 2020

  • HHL (Xiangyu Jin, Shuling Wang, Bohua Zhan, Naijun Zhan)
  • KeYmaera 3 (Andre Platzer)
  • KeYmaera X (Stefan Mitsch, Andre Platzer, Andrew Sogokon, Yong Kiam Tan)