1. A computer-implemented method of determining an abstraction for a computer program, the method comprising: accessing within a computer a representation of the computer program, the representation comprising a directed graph; reducing a plurality of nodes within the directed graph to a single node, the plurality of nodes including only less than all nodes within the directed graph, thereby generating an abstraction of the directed graph; choosing a path in the abstraction which includes the single node; determining if the path is an infeasible path that represents a process that would not be possible for execution of the computer program; upon determining the path is infeasible, generating one or more constraints to refine the abstraction such that a refined abstraction can be generated that applies the constraints to effectively eliminate the infeasible path from the refined abstraction; and generating the refined abstraction by applying the one or more constraints to the abstraction.