Friendly Competition

Call for Participation

ARCH-COMP 2019
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:
arch-2019@easychair.org

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.

Results

Reports of the 2018 results can be found in the ARCH proceedings.

Reports on the 2017 results can be found in the ARCH proceedings.

Repeatability Packages

Repeatability packages of all years can be found here.

Participants

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)