Towards a set-based IVP solver for ODEs on the GPU (REC 2026 - 11th International Workshop on Reliable Engineering Computing: Reliability Computations in a Data and Model-Driven World, 2026)
Reachability analysis is a key component of (formal) verification techniques for cyber-physical systems subject to uncertainty, as it enables the computation of sets of states that the system can reach over time. However, such methods are often computationally expensive, making algorithmic and implementation-level optimizations essential. In this paper, we propose a verified interval-based ODE solver for reachability analysis, based on the classical fourth-order Runge–Kutta scheme and designed to execute entirely within a single GPU kernel. This enables efficient subdivision strategies to mitigate overestimation while supporting the parallel propagation of a large number of subboxes. Using the Van der Pol oscillator as a benchmark, we demonstrate the applicability of the proposed approach and compare its performance with non-verified GPU-based uncertainty propagation techniques derived from Müller-type theorems, as well as with the CPU-based reference tool DynIbex.