We propose a novel verification method for high-dimensional feed-forward neural networks governed by ReLU, Sigmoid and Tanh activation functions. We show that the method is complete for ReLU networks and sound for other activation functions. The technique extends symbolic interval propagation by using gradient-descent to locate counter-examples from spurious solutions generated by the associated LP problems. The approach includes a novel adaptive splitting strategy intended to refine the nodes with the greatest impact on the output of the network. The resulting implementation, called VERINET, achieved speed-ups of approximately one order of magnitude for safe cases and three orders of magnitude for unsafe cases on MNIST models against SoA complete methods. VERINET could verify networks of over 50,000 ReLU nodes trained on the CIFAR-10 data-set; these are larger than networks that could previously verified via complete methods.