Tool presentation: When formally verifying models of cyber-physical systems, it is obviously important that their verification results can be transferred to all previous observations of the modeled systems. Our tool CORA makes it possible to transfer safety properties by checking whether all measurements of the real system lie in the set of reachable outputs of the corresponding model -- we call this reachset conformance checking. In addition, we provide strategies to establish reachset conformance by injecting nondeterminism in models. This can be seen as some form of system identification, where instead of finding the most likely parameters, we compute a set of parameter values -- not only for the model dynamics but also for the set of disturbances and measurement errors -- to establish reachset conformance. By replacing real measurements with simulation results from a high-fidelity model, one can also check whether a high-fidelity model conforms to a simple model. We demonstrate the usefulness of reachset conformance by several use cases.
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 2023. In the fifth edition of this AINNCS category at ARCH-COMP, three tools have been applied to solve ten different benchmark problems, which are CORA, JuliaReach and NNV. In reusing the benchmarks from the last iteration, we demonstrate the continuous progress in developing these tools: Two out of three tools can verify more instances than in the 2022 iteration. A novelty of this year’s iteration is the shared computation hardware that allows for a fairer comparison among the participants.
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. Given that the tools for stochastic models are at their early stages of development compared to those of non-probabilistic models, the main focus is to report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between the efficiency of the implemented techniques. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2023.
This report presents the results from the 2023 friendly competition in the ARCH workshop for the falsification of temporal logic specifications over Cyber-Physical Systems. We describe the benchmark models selected to compare the tools and the competition settings and provide background on the participating teams and tools. Finally, we present and discuss our results.
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 2023. This year, 6 tools participated: Ariadne, CORA, DynIbex, JuliaReach, KeYmaera X and Verse (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.
