ARCH-COMP24: Papers with Abstracts

Papers
ARCH-COMP24 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 2024. 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. Compared to the last competition in 2022, three new benchmarks have been added (Nuclear Reactor System, FDDI, Ring-Shape Fischer’s Protocol). The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for.
ARCH-COMP24 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics Matthias Althoff, Marcelo Forets, Christian Schilling and Mark Wetzlinger Abstract. We present the results of the ARCH1 2024 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its eighth 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-COMP24 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, Christian Schilling, Joris Tillet and Mark Wetzlinger 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 2024. 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 six benchmark problems, two of them featuring 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-COMP24 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants Diego Manzanas Lopez, Matthias Althoff, Luis Benet, Clemens Blab, Marcelo Forets, Yuhao Jia, Taylor T Johnson, Manuel Kranzl, Tobias Ladner, Lukas Linauer, Philipp Neubauer, Sophie Neubauer, 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 2024. In the 8th edition of this AINNCS category at ARCH-COMP, five tools have been applied to solve 12 benchmarks, which are CORA, CROWN-Reach, GoTube, JuliaReach, and NNV. This is the year with the largest interest in the community, with two new, and three previous participants. Following last year’s trend, despite the additional challenges presented, the verification results have improved year-over-year. In terms of computation time, we can observe that the previous participants have improved as well, showing speed-ups of up to one order of magnitude, such as JuliaReach on the TORA benchmark with ReLU controller, and NNV on the TORA benchmark with both heterogeneous controllers.
ARCH-COMP 2024 Category Report: Falsification Tanmay Khandait, Federico Formica, Paolo Arcaini, Surdeep Chotaliya, Georgios Fainekos, Abdelrahman Hekal, Atanu Kundu, Ethan Lew, Michele Loreti, Claudio Menghi, Laura Nenzi, Giulia Pedrielli, Jarkko Peltomäki, Ivan Porres, Rajarshi Ray, Valentin Soloviev, Ennio Visconti, Masaki Waga and Zhenya Zhang Abstract. This report presents the results from the falsification category of the 2024 competition in the Applied Verification for Continuous and Hybrid Systems (ARCH) workshop. The report summarizes the competition rules and settings, the benchmark models for the tool comparison, and provides background on the participating teams and tools. Finally, it presents and discusses the results of the competition.
Stability Verification of an Industrial Switched PI Control Systems Stylianos Basagiannis, Ludovico Battista, Anna Becchi, Alessandro Cimatti, Georgios Giantamidis, Sergio Mover, Alberto Tacchella, Stefano Tonetta and Vassilios Tsachouridis Abstract. Benchmark Proposal: In this paper, we propose a benchmark that addresses the chal- lenge of verifying Global Asymptotic Stability for a switched control of a turbofan engine. The control switches among two Proportional-Integral (PI) controllers and is parametrized by the reference values used to stabilize the output. We formulate the mathematical model as an affine switched system with a parametric affine term. The verification problems are, on one hand, to prove symbolically the stability of the system for specific reference values, and, on the other hand, to synthesize a region of parameters for which the stability is guaranteed. We report on previous works partially solving these problems.
Randomized Generation of Arbitrarily Difficult Verification Benchmarks for Linear Time-Invariant Systems Mark Wetzlinger and Matthias Althoff Abstract. Benchmark proposal: The verification of uncertain linear systems is a fundamental building block for the analysis of complex cyber-physical systems. While there exist many advanced tools for numerical analysis, their evaluation is to date limited by selected bench- marks. To better understand the strengths and weaknesses of formal verification algorithms for linear systems, we propose a randomized generation of verification benchmarks in this paper. To this end, we leverage a reachability algorithm that can compute reachable sets with arbitrary precision. By placing unsafe sets exactly at the boundary of the computed outer and inner approximations, we are able to generate random verification tasks of ar- bitrary difficulty by changing the precision of the reachability analysis. We validate our approach by verifying and falsifying increasingly complex generated benchmarks using a state-of-the-art verification algorithm.
Implementation of Polyhedral Operations in CORA 2024 Mark Wetzlinger, Viktor Kotsev, Adrian Kulmburg and Matthias Althoff Abstract. Tool presentation: Polyhedra are a common set representation with widespread appli- cations in many areas of research, including convex geometry, reachability analysis, and invariant set computation. Their popularity stems from a tight relation to linear program- ming. Apart from some basic set operations with analytic formulae, the implementation of many polyhedral set operations in tools is not well documented. For this reason, we describe the evaluation of common set operations on polyhedra, including their runtime complexity, and provide an overview of their implementation as a dedicated class in the MATLAB tool Continuous Reachability Analyzer (CORA) for set-based computing. In particular, we highlight the handling of unbounded and degenerate sets. Finally, we com- pare our implementation to the popular multi-parametric toolbox.