A major obstacle to using deep neural networks in safety-critical systems is the great difficulty of providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique uses a statisfiability modulo theories (SMT) framework coupled with the simplex linear programming method, extended to handle piecewise-linear functions. The extension allows the procedure to reason natively about constructs such as rectified linear units and max pooling nodes found in neural networks. We present the results of using our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Our technique can successfully prove properties of this network that are beyond the reach of other techniques.