Friendly Competition

Call for Participation

3rd International Competition on Verifying Continuous and Hybrid Systems

Call for Participation

1. Join a group that treats problems similar to yours (by Jan 20).
- 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 Feb 24).
- 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 Mar 24).
- Evaluation chair signals approved results.

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

5. Reports are presented (Apr 15)
- presentation at ARCH workshop, part of CPS-IoT Week in Montreal, Canada.
(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 ParisTech
Matthias Althoff, Technische Universitat Munchen

Publicity Chair:
Sergiy Bogomolov, Australian National 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 2019

  • 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 2019

  • CORA (Nikolas Kochdumper, Matthias Althoff)
  • CORA/SX (Goran Frehse)
  • HyDRA (Stefan Schupp)
  • Hylaa (Stanley Bak)
  • Hylaa-Continuous (Stanley Bak)
  • JuliaReach (Marcelo Forets, Christian Schilling)
  • SpaceEx (Goran Frehse)
  • XSpeed (Rajarshi Ray)

Nonlinear Dynamics (lead: Fabian Immler); updated April 2019

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

AI category (new, lead: Taylor Johnson); updated February 2019

  • ASU (Georgios Fainekos and Shakiba Yaghoubi)
  • Berkeley (Sanjit Seshia, Tommaso Dreossi, Somil Bansal, and Shromona Ghosh)
  • nnv (Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Weiming Xiang, Miklos Maroti, and Taylor T. Johnson)
  • NSVerify (Michael Akintunde and Alessio R. Lomuscio)
  • Sherlock (Sriram Sankaranarayanan, Souradeep Dutta, Susmit Jha, and Ashish Tiwari)
  • SMC (Yasser Shoukry, Haitham Khedr, Xiawou Sun)
  • Verisig (Radoslav Ivanov, James Weimer, Insup Lee)

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

  • 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 2019

  • BACH (Lei Bu)
  • HyDRA (Stefan Schupp)
  • XSpeed (Rajarshi Ray)

Falsification (lead: Georgios Fainekos); updated April 2019

  • Breach (Alexandre Donze)
  • falsify (Yoriyuki Yamagata)
  • FalStar (Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Yoriyuki Yamagata)
  • S-TaLiRo (Georgios Fainekos, Shakiba Yaghoubi, Logan Mathesen, Giulia Pedrielli)

Hybrid Programs (lead: Stefan Mitsch); updated April 2019

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