22. A device-implemented method, comprising: receiving computer code, the receiving being performed by the device; performing a static verification analysis of the computer code to locate a point, in the computer code, that, under at least one set of states of variables in the computer code, causes an error in an execution of the computer code, the static verification analysis being performed by analyzing a first plurality of possible execution paths of the computer code, the first plurality of possible execution paths being determined based on an over-approximation of states, and the performing being performed by the device; traversing, from the located point and in a backward direction, through a second plurality of possible execution paths, the second plurality of possible execution paths being determined based on an under-approximation of the states that were over-approximated, and the traversing being performed by the device; analyzing the located point using an empiric analysis technique based on semantic information for the computer code, the analyzing the located point being performed by the device; determining, based on the traversing, a second point in the computer code as a potential cause of the error, the determining being performed by the device; classifying, based on the traversing and the analyzing the located point, the second point as a first error classification, when the error is caused by code of the received computer code, or a second error classification, when the error is caused by an input to the computer code, the classifying being performed by the device; and storing information identifying the classification and information that describes the second point in the computer code, the storing being performed by the device.
22. A device-implemented method, comprising: receiving computer code, the receiving being performed by the device; performing a static verification analysis of the computer code to locate a point, in the computer code, that, under at least one set of states of variables in the computer code, causes an error in an execution of the computer code, the static verification analysis being performed by analyzing a first plurality of possible execution paths of the computer code, the first plurality of possible execution paths being determined based on an over-approximation of states, and the performing being performed by the device; traversing, from the located point and in a backward direction, through a second plurality of possible execution paths, the second plurality of possible execution paths being determined based on an under-approximation of the states that were over-approximated, and the traversing being performed by the device; analyzing the located point using an empiric analysis technique based on semantic information for the computer code, the analyzing the located point being performed by the device; determining, based on the traversing, a second point in the computer code as a potential cause of the error, the determining being performed by the device; classifying, based on the traversing and the analyzing the located point, the second point as a first error classification, when the error is caused by code of the received computer code, or a second error classification, when the error is caused by an input to the computer code, the classifying being performed by the device; and storing information identifying the classification and information that describes the second point in the computer code, the storing being performed by the device. 24. The device-implemented method of claim 22 , where determining the second point in the computer code includes: determining the second point as a point, in the computer code, that includes an input, a variable assignment, a variable declaration, or a function return value.