1. A computer-implemented method comprising: syntactically analyzing a computer program to identify bug-prone portions of the computer program that correspond to one or more bug patterns, wherein the identified bug-prone portions are suspected of including a bug, wherein the identified bug-prone portions either include a bug or do not include a bug; performing, by a processor, verification of the computer program, wherein the verification comprises traversing a control flow graph of the computer program and tracking symbolic values of variables of the computer program, wherein said performing comprises directing the traversal of the control flow graph to nodes of the control flow graph that correspond to the identified bug-prone portions, wherein an edge associated with a larger number of control flow paths of the control flow graph which correspond to the one or more bug patterns is assigned a higher priority than another edge associated with a smaller number of control flow path which corresponds to the one or more bug patterns; and whereby the bug-prone portions of the computer program, which were identified during said syntactically analyzing, are prioritized to be verified before non-bug-prone portions of the computer program, which were not identified as bug-prone during said syntactically analyzing.