  Deep convolutional neural networks have been widely employed as an effective
technique to handle complex and practical problems. However, one of the
fundamental problems is the lack of formal methods to analyze their behavior.
To address this challenge, we propose an approach to compute the exact
reachable sets of a network given an input domain, where the reachable set is
represented by the face lattice structure. Besides the computation of reachable
sets, our approach is also capable of backtracking to the input domain given an
output reachable set. Therefore, a full analysis of a network's behavior can be
realized. In addition, an approach for fast analysis is also introduced, which
conducts fast computation of reachable sets by considering selected sensitive
neurons in each layer. The exact pixel-level reachability analysis method is
evaluated on a CNN for the CIFAR10 dataset and compared to related works. The
fast analysis method is evaluated over a CNN CIFAR10 dataset and VGG16
architecture for the ImageNet dataset.
