1. A device-implemented method, comprising: receiving computer code, at the device; performing a static verification analysis of the computer code to locate a point in the code that, under at least one set of states of variables in the computer code, causes an error in the execution of the computer code, where the static analysis is performed by analyzing a first plurality of possible execution paths of the computer code based on an over-approximation of states, where the performing is performed by the device; back-propagating, by the device and from the located point, through a second plurality of possible execution paths, where the second plurality of possible execution paths is obtained based on an under-approximation of the states that were over-approximated, where the back-propagating is performed by the device; determining, based on the back-propagation, a second point in the computer code as a potential cause of the error, the determining being performed by the device; and storing output information to describe the second point in the computer code, the storing being performed by the device.