Deep neural networks have become an integral component of many systems for which ensuring safety, robustness, and reliability is crucial. In this talk, we present an abstract interpretation based method for efficient verification of a class of properties called differential properties. While we focus on network equivalence as the canonical example, other interesting properties concerning input sensitivity and stability can also be cast as differential properties. Our key insight is in deriving sound abstractions that relate the intermediate results of nonlinear computations of two structurally-similar neural networks, to accurately bound their maximum difference over all inputs. We also propose automated synthesis techniques for generating linear abstractions of arbitrary nonlinear functions, to handle architectures beyond feed-forward ReLU networks.