ARCH22: Papers with Abstracts

Abstract. Tool presentation: Ellipsoids are a broadly applied set representation for formal anal- yses, such as set-based observers, or reachability analysis. While ellipsoids are not closed under frequently used set operations like Minkowski sum or intersection, their widespread popularity can be attributed to their compact numerical representation and intuitive na- ture. As a result, there already exist toolboxes that implement many operations for el- lipsoids. That said, most are either no longer maintained, or implement only a subset of necessary ellipsoidal operations. Thus, we implement all common set operations, as well as recent research results on ellipsoids as a class in the Continuous Reachability Analyzer (CORA) - a free MATLAB toolbox for continuous reachability analysis. Previously, CORA already contained implementations for many ellipsoidal operations, which, however, were lacking in speed, accuracy, and functionality. Here, we describe the implementation of the ellipsoid class in CORA and compare it against the popular, but no longer maintained, Ellipsoidal Toolbox (ET).

Abstract. This paper proposes a benchmark for a controller of a pacemaker device developed as part of the course “SFWRENG 3MD3 - Safe Software-Intensive Medical Devices” pro- vided at McMaster University. The benchmark includes two alternative Simulink® models, developed by two different groups of students. Each model comes with a requirement for- malized in Signal Temporal Logic (STL). We also present the testing results obtained using S-TaLiRo, a well-known testing framework for Simulink® models.

Abstract. Benchmark proposal: Safe renewable energy systems are becoming increasingly impor- tant to combat climate change. Electric utility companies often use conservative approaches to feed in renewable energy to ensure a safe operation due to a lack of advanced analysis techniques. So far, mostly simulations are used in practice to safeguard the system against certain contingencies, which cannot provide guaranties. While so-called direct methods based on Lyapunov functions potentially provide formal guarantees, they are not really used in practice due to the difficulty of finding Lyapunov functions of larger models. How- ever, we believe that reachability analysis can be conveniently used to ensure correctness, because it can be performed automatically without expert knowledge. To analyze the state of the art in this important application area, we provide a tool that automatically gener- ates benchmark problems from a given system description. We also provide problems of different difficulty and for different types of analysis, namely transient stability analysis, verifying regions of attraction, and verifying robustness against uncertain power demand and production. Exemplary solutions of benchmark problems are shown as well.

Abstract. This report presents the results of a friendly competition for formal verification of con- tinuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Sys- tems (ARCH) in 2022. In this edition, five tools have been applied to solve six different benchmark problems in the category for piecewise constant dynamics: BACH, PHAVer, PHAVerLite, 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.

Abstract. We present the results of the ARCH1 2022 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its sixth edition, two tools have been applied to solve nine 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, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

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 2022. This year, 6 tools Ariadne, CORA, DynIbex, JuliaReach, Kaa and KeYmaera X (in alphabetic order) participated. 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.

Abstract. This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year’s edition of the competition. In comparison with tools on non-probabilistic models, the tools for stochastic models are at the early stages of development that do not allow full competition on a standard set of benchmarks. We report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between efficiency of the implemented techniques. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2022.

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 more 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 2022. In the fourth edition of this AINNCS category at ARCH-COMP, four tools have been applied to solve 10 different benchmark problems. There are two new participants: CORA and POLAR, and two previous participants: JuliaReach and NNV. The goal of this report is to be a snapshot of the current landscape of tools and the types of benchmarks for which these tools are suited. The results of this iteration significantly outperform those of any previous year, demonstrating the continuous advancement of this community in the past decade.

Abstract. This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the
ARCH-COMP Friendly Competition 2022. The characteristic features of the HSTP cate- gory remain as in the previous editions [MST+18, MST+19, MMJ+20], it focuses on flexi- bility 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 verifica- tion 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.

Abstract. This report presents the results from the 2022 friendly competition in the ARCH work- shop for the falsification of temporal logic specifications over Cyber-Physical Systems. We briefly describe the competition settings, which have been inherited and adapted from the previous years, give background on the participating teams and tools, and discuss the selected benchmarks. In this year’s competition, in addition to the result validation introduced in the previous year, we change the experimental settings for a better account of the difficulty of benchmarks and for a better comparability between the tools.

Abstract. The repeatability evaluation for the 6th International Competition on Verifying Con- tinuous and Hybrid Systems (ARCH-COMP’22) is summarized in this report. The compe- tition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2022, affiliated with the 41st International Conference on Computer Safety, Reliability and Security (SAFECOMP’22). In its sixth edition, 25 tools had submit- ted artifacts through a Git repository for the repeatability evaluation, which were applied to solve benchmark instances through 7 competition categories. The majority of partic- ipants adhered to the specifications of this year’s repeatability evaluation, which was to submit scripts to automatically install and execute tools in containerized virtual environ- ments (specifically Dockerfiles to execute within Docker containers). Some categories used performance evaluation information from a common execution platform. The repeatability results represent a snapshot of current tools and the types of benchmarks on which they are well suited, and so that others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing of being repeatable.