  Implementations of artificial neural networks (ANNs) might lead to failures,
which are hardly predicted in the design phase since ANNs are highly parallel
and their parameters are barely interpretable. Here, we develop and evaluate a
novel symbolic verification framework using incremental bounded model checking
(BMC), satisfiability modulo theories (SMT), and invariant inference, to obtain
adversarial cases and validate coverage methods in a multi-layer perceptron
(MLP). We exploit incremental BMC based on interval analysis to compute
boundaries from a neuron's input. Then, the latter are propagated to
effectively find a neuron's output since it is the input of the next one. This
paper describes the first bit-precise symbolic verification framework to reason
over actual implementations of ANNs in CUDA, based on invariant inference,
therefore providing further guarantees about finite-precision arithmetic and
its rounding errors, which are routinely ignored in the existing literature. We
have implemented the proposed approach on top of the efficient SMT-based
bounded model checker (ESBMC), and its experimental results show that it can
successfully verify safety properties, in actual implementations of ANNs, and
generate real adversarial cases in MLPs. Our approach was able to verify and
produce adversarial examples for 85.8% of 21 test cases considering different
input images, and 100% of the properties related to covering methods. Although
our verification time is higher than existing approaches, our methodology can
consider fixed-point implementation aspects that are disregarded by the
state-of-the-art verification methodologies.
