  This paper presents an approach for verifying the behaviour of nonlinear
Artificial Neural Networks (ANNs) found in cyber-physical safety-critical
systems. We implement a dedicated interval constraint propagator for the
sigmoid function into the SMT solver iSAT and compare this approach with a
compositional approach encoding the sigmoid function by basic arithmetic
features available in iSAT and an approximating approach. Our experimental
results show that the dedicated and the compositional approach clearly
outperform the approximating approach. Throughout all our benchmarks, the
dedicated approach showed an equal or better performance compared to the
compositional approach.
