Friendly Competition

Call for Participation

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:

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.


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.


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)