ARCH26: Papers with Abstracts

Papers
SpaceEx Hybrid Models with LTL Properties Ludovico Battista, Stefano Tonetta and Gianni Zampedri Abstract. The automated verification of hybrid systems has traditionally focused on safety and reachability properties. However, verifying liveness and general Linear Temporal Logic (LTL) properties is essential in many applications. This paper proposes a new benchmark suite for the ARCH competition, utilizing an LTL-enhanced extension of the standard SpaceEx model format. Our suite consists of several hybrid automata featuring linear and non-linear dynamics, ranging from 2D scalable models to 10D vehicle drivetrain systems. We provide a detailed formalization of a car overtaking maneuver to demonstrate how temporal specifications are encoded directly within the model files. To establish a baseline for the competition, we present experimental results obtained using the VeriLHyS tool. These benchmarks are intended to serve as a foundation for cross-tool comparisons and to foster the development of LTL support in other tools.
ARCH-COMP26 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking Lei Bu, Atanu Kundu, Rajarshi Ray, Rayan Mazouz and Yuhui Shi Abstract. This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2026. In this edition, four tools have been applied to solve eleven different benchmark problems in the category for piecewise constant dynamics: BACH, SAT-Reach, StochasticBarrier.jl, and XSpeed. Compared to the last competition in 2025, two new benchmarks have been added (Lynch and Temperature). The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.
ARCH-COMP26 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics Matthias Althoff, Alessandro Carraro, Marcelo Forets, Maximilian Perschl and Christian Schilling Abstract. We present the results of the ARCH 2026 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its tenth edition, two tools participated to solve eight different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA and JuliaReach. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools.
ARCH-COMP26 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics Luca Geretti, Julien Alexandre Dit Sandretto, Matthias Althoff, Luis Benet, Pieter Collins, Marcelo Forets, Stefan Mitsch, Maximilian Perschl, Christian Schilling, Joris Tillet and Ben Wooding Abstract. We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2026. This year, 6 tools participated: Ariadne, CORA, DynIbex, JuliaReach, KeYmaera X and PRoTECT (in alphabetic order). These tools are applied to solve reachability analysis problems on seven benchmark problems, two of them featuring some aspects of hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.
ARCH-COMP26 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants Samuel Sasaki, Ben Wooding, Taylor T. Johnson, Matthias Althoff, Luis Benet, Samuel Coogan, Marcelo Forets, Akash Harapanahalli, Lukas Koller, Tobias Ladner, Christian Schilling, Huan Zhang and Xiangru Zhong Abstract. This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with artificial intelligence (AI) components. Specifically, machine learning (ML) components in cyber-physical systems (CPS), such as feedforward neural networks used as feedback controllers in closed-loop systems, are considered, which is a class of systems classically known as intelligent control systems, or in more modern and specific terms, neural network control systems (NNCS). We broadly refer to this category as AI and NNCS (AINNCS). The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2026. In this edition of the AINNCS category at ARCH-COMP, four tools have been applied to solve 12 benchmarks, which are CORA, CROWN-Reach, immrax, and JuliaReach.
ARCH-COMP26 Category Report: Hybrid Systems Theorem Proving Stefan Mitsch, Xiangyu Jin, Shuling Wang and Bohua Zhan Abstract. This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2026. HSTP focuses on flexibility of programming languages as structuring principles for hybrid systems, unambiguity and precision of program semantics, and mathematical rigor of logical reasoning principles. The benchmark set includes nonlinear and parametric continuous and hybrid systems and hybrid games, each in three modes: fully automatic verification, semi-automatic verification from proof hints, proof checking from scripted tactics. This instance of the competition focuses on presenting the differences between the provers on a subset of the benchmark examples.
ARCH-COMP26 Category Report: Falsification Tanmay Khandait, Paolo Arcaini, Georgios Fainekos, Federico Formica, Sauvik Gon, Ali Kaya, Atanu Kundu, Deyun Lyu, Claudio Menghi, Giulia Pedrielli, Ivan Porres, Rajarshi Ray, Quinn Thibeault, Masaki Waga and Zhenya Zhang Abstract. We report the results from the falsification category of the 2026 Applied Verification for Continuous and Hybrid Systems (ARCH) competition. We summarize the rules for this year’s competition, the experimental settings, and benchmark models. We provide background on the participating teams and tools. Finally, we present and discuss the results of this year's competition.
ARCH-COMP26 Repeatability Evaluation Report Nico Holzinger and Tobias Ladner Abstract. The repeatability evaluation for the 13th International Competition on Verifying Continuous and Hybrid Systems (ARCH-COMP’26) is summarized in this report. The competition was held as part of the Applied Verification for Continuous and Hybrid Systems (ARCH) workshop in 2026. In its 13th edition, participants submitted their tools via an automated evaluation system developed over recent years. Each submission includes a Dockerfile and the necessary scripts for running the tool, enabling consistent execution in a containerized environment with all dependencies preinstalled. This setup improves comparability by running all tools on the same hardware. Submissions and results are automatically synchronized with a Git repository for repeatability evaluation and long-term archiving. We plan to further extend the evaluation system by refining the submission pipeline, aiming to enable automated evaluation across all competition categories.