  This paper presents a novel approach to ensure the safety of continuous-time
linear dynamical systems controlled by a neural network (NN) based
state-feedback. Our method capitalizes on the use of continuous piece-wise
affine (PWA) activation functions (e.g. ReLU) which render the NN a PWA
continuous function. By computing the affine regions of the latter and applying
Nagumo's theorem, a subset of boundary points can effectively verify the
invariance of a potentially non-convex set. Consequently, an algorithm that
partitions the state space in affine regions is proposed. The scalability of
our approach is thoroughly analyzed, and extensive tests are conducted to
validate its effectiveness.
