  We introduce DeepCert, a tool-supported method for verifying the robustness
of deep neural network (DNN) image classifiers to contextually relevant
perturbations such as blur, haze, and changes in image contrast. While the
robustness of DNN classifiers has been the subject of intense research in
recent years, the solutions delivered by this research focus on verifying DNN
robustness to small perturbations in the images being classified, with
perturbation magnitude measured using established Lp norms. This is useful for
identifying potential adversarial attacks on DNN image classifiers, but cannot
verify DNN robustness to contextually relevant image perturbations, which are
typically not small when expressed with Lp norms. DeepCert addresses this
underexplored verification problem by supporting:(1) the encoding of real-world
image perturbations; (2) the systematic evaluation of contextually relevant DNN
robustness, using both testing and formal verification; (3) the generation of
contextually relevant counterexamples; and, through these, (4) the selection of
DNN image classifiers suitable for the operational context (i)envisaged when a
potentially safety-critical system is designed, or (ii)observed by a deployed
system. We demonstrate the effectiveness of DeepCert by showing how it can be
used to verify the robustness of DNN image classifiers build for two benchmark
datasets (`German Traffic Sign' and `CIFAR-10') to multiple contextually
relevant perturbations.
