ARCH25: Papers with Abstracts

Papers
ARCH-COMP25 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking Lei Bu, Atanu Kundu, Rajarshi Ray 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 2025. In this edition, three tools have been applied to solve nine different benchmark problems in the category for piecewise constant dynamics: BACH, SAT-Reach, and XSpeed. 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-COMP25 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics Matthias Althoff, Marcelo Forets, Maximilian Perschl and Christian Schilling Abstract. We present the results of the ARCH 2025 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its ninth 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-COMP25 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, Ismail Patel, Maximilian Perschl, Christian Schilling and Joris Tillet 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 2025. This year, 5 tools participated: Ariadne, CORA, DynIbex, JuliaReach and KeYmaera X (in alphabetic order). These tools are applied to solve reachability analysis problems on seven benchmark problems, three 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-COMP25 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants Diego Manzanas Lopez, Matthias Althoff, Luis Benet, Samuel Coogan, Marcelo Forets, Akash Harapanahalli, Taylor T. Johnson, 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 2025. In this edition of the AINNCS category at ARCH-COMP, five tools have been applied to solve 12 benchmarks, which are CORA, CROWN-Reach, immrax, JuliaReach, and NNV. For the second year in a row, we have the largest interest in the community, with four previous participants and one new participant, immrax. In reusing the hardware infrastructure and benchmarks from last year, we can observe comparable results from previous improvements, with slight improvements in computation time by CORA and NNV in selected benchmarks. A novelty of this year is the different problem abstraction between immrax and the rest of tools, leading to result disparities in 2 benchmarks: Single Pendulum and Attitude Control.
ARCH-COMP25 Category Report: Stochastic Models Alessandro Abate, Omid Akbarzadeh, Henk A.P. Blom, Sofie Haesaert, Sina Hassani, Abolfazl Lavaei, Frederik Baymler Mathiesen, Rahul Misra, Amy Nejati, Mathis Niehage, Fie Ørum, Anne Remke, Behrad Samari, Ruohan Wang, Rafal Wisniewski, Ben Wooding and Mahdieh Zaker Abstract. This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. In particular, this report introduces three recently developed software tools, a new water distribution network benchmark, and a collection of simplified benchmarks intended to facilitate further comparisons among tools that were previously not directly comparable. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2025.
ARCH-COMP25 Category Report: Hybrid Systems Theorem Proving Stefan Mitsch, Ismail Patel, Hari Hara Sudhan Kannan, Xiangyu Jin, Bohua Zhan and Shuling Wang Abstract. This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2025. 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-COMP25 Category Report: Falsification Tanmay Khandait, Deyun Lyu, Paolo Arcaini, Georgios Fainekos, Federico Formica, Sauvik Gon, Abdelrahman Hekal, Atanu Kundu, Claudio Menghi, Giulia Pedrielli, Rajarshi Ray, Quinn Thibeault, Masaki Waga and Zhenya Zhang Abstract. We report the results from the falsification category of the 2025 competition in the Applied Verification for Continuous and Hybrid Systems (ARCH) workshop. 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 the competition.
ARCH-COMP25 Repeatability Evaluation Report Tobias Ladner Abstract. The repeatability evaluation for the 9th International Competition on Verifying Continuous and Hybrid Systems (ARCH-COMP’25) is summarized in this report. The competition was held as part of the Applied Verification for Continuous and Hybrid Systems (ARCH) workshop in 2025. In its 9th 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.