Eddie B. L. Filho

Luiz Sena, Erickson Alves, Iury Bessa et al.

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.

Daniel P. M. de Mello, Mauro L. de Freitas, Lucas C. Cordeiro et al.

In the digital signal processing (DSP) area, one of the most important tasks is digital filter design. Currently, this procedure is performed with the aid of computational tools, which generally assume filter coefficients represented with floating-point arithmetic. Nonetheless, during the implementation phase, which is often done in digital signal processors or field programmable gate arrays, the representation of the obtained coefficients can be carried out through integer or fixed-point arithmetic, which often results in unexpected behavior or even unstable filters. The present work addresses this issue and proposes a verification methodology based on the digital-system verifier (DSVerifier), with the goal of checking fixed-point digital filters w.r.t. implementation aspects. In particular, DSVerifier checks whether the number of bits used in coefficient representation will result in a filter with the same features specified during the design phase. Experimental results show that errors regarding frequency response and overflow are likely to be identified with the proposed methodology, which thus improves overall system's reliability.

Renato B. Abreu, Lucas Cordeiro, Eddie B. L. Filho

The implementation of digital filters in processors based on fixed-point arithmetic can lead to problems related to the finite word-length. In particular, the processing of signals in such filters can produce overflows and unwanted noise caused by quantization and round off effect during the accumulative addition and multiplication operations. In this paper, we describe a new approach to verify digital filters using an off-the-shelf bounded model checker called ESBMC, which supports full C/C++ and is based on satisfiability modulo theories solvers. In particular, we are able to verify the occurrence of overflows, limit cycles, and time constraints based on a discrete-time model implemented in C. The experiments show that the proposed approach can be used to verify potential problems in fixed-point implementation of digital filters and it can thus be effective in finding realistic design errors.