ARCH-COMP24 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking

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.