Advancing Verification of Continuous and Hybrid Systems
ARCH-COMP is the friendly international competition for the verification of continuous and hybrid systems. Held annually since 2017 as part of the ARCH workshop, it brings together tool developers across seven categories — from reachability analysis to falsification, stochastic models, and neural network control — on a shared, reproducible set of benchmarks.
About ARCH-COMP
ARCH-COMP is the annual friendly competition of the ARCH workshop (Applied Verification for Continuous and Hybrid Systems), which since 2014 has focused on transferring verification techniques for cyber-physical systems from theory to practice. Since 2017, the competition has evaluated and compared state-of-the-art verification tools on a curated, openly available collection of benchmarks.
Each category is coordinated by dedicated organizers who agree on benchmarks and metrics with the participants. All results are made repeatable: participants submit installation and execution scripts (typically containerized) so that every reported result can be independently reproduced. Category reports are published each year in the EPiC Series in Computing.
Competition Categories
ARCH-COMP is organized into seven categories, each coordinated by dedicated leads who agree on benchmarks and metrics with the participants. Not every category runs in every edition.
Linear Dynamics
Reachability and safety verification of continuous and hybrid systems with linear (affine) dynamics.
Lead: Matthias Althoff (TU Munich)
Nonlinear Dynamics
Reachability analysis for continuous and hybrid systems governed by nonlinear ODEs.
Lead: Luca Geretti (University of Verona)
Piecewise Constant Dynamics
Verification of hybrid automata with piecewise constant (rectangular) dynamics.
Lead: Lei Bu (Nanjing University)
AI & Neural Network Control (AINNCS)
Verification of closed-loop systems whose controllers are neural networks.
Lead: Taylor T. Johnson (Vanderbilt University)
Stochastic Models
Verification and controller synthesis for stochastic and probabilistic dynamical systems.
Lead: Abolfazl Lavaei (Newcastle University)
Falsification
Finding counterexamples to temporal-logic specifications for cyber-physical systems.
Lead: Ivan Porres (Åbo Akademi University)
Hybrid Programs
Deductive verification and theorem proving for hybrid programs.
Lead: Stefan Mitsch (DePaul University)
Organizers
ARCH-COMP is run by a team of general chairs together with the leads of each category.
General Chairs
Goran Frehse (ENSTA, IP Paris), Matthias Althoff (TU Munich)
Evaluation Chairs
Taylor T. Johnson (Vanderbilt University), Tobias Ladner (TU Munich), Nico Holzinger (TU Munich)
Publication Chair
Luca Geretti (University of Verona)
Get Involved
Join the Community
Interested in participating or contributing to ARCH-COMP? We welcome tool developers, benchmark proposers, and researchers working on the verification of continuous, hybrid, stochastic, and learning-enabled cyber-physical systems.
- Email the organizers to get started
- Contribute benchmarks and tools to a category
- Submit a repeatability package
- Participate in the annual competition