Program abstraction based on program control
AssigneeMicrosoft Corporation
InventorsSumit Gulwani, Akash Lal
Life of this patent
Estimating the term…
Abstract
Embodiments described herein relate to determining an abstraction of a computer program and to the refinement of an abstraction of a computer program. The computer program may be a sequential program or may be a concurrent (parallel) program. A directed graph represents a computer program and may be the cross product of threads within a concurrent program. Nodes within a representation of a program are reduced to a single node to produce an abstraction. An abstraction may be refined by determining constraints that produce a refined abstraction that does not comprise infeasible paths.
Claims20
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;
- and
- 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.
A computer-implemented method of refining an abstraction for a computer program, the method comprising:
- choosing a path in the abstraction;
- determining if the path is an infeasible path;
- upon determining the path is infeasible, generating one or more constraints to refine the abstraction such that the refined abstraction does not comprise the infeasible path;
- and
- determining a refined abstraction by applying the constraints to the abstraction.
A computer program product comprising one or more computer-readable storage media having encoded thereon computer executable instructions which, when executed, implement a method of determining an abstraction for a computer program, the method comprising:
- determining a representation of the computer program, the representation comprising a directed graph;
- reducing one or more nodes within the directed graph to a single node.
- choosing a path in the abstraction;
- determining if the path is an infeasible path;
- upon determining the path is infeasible, generating one or more constraints to refine the abstraction such that the refined abstraction does not comprise the infeasible path;
- and
- determining a refined abstraction by applying the constraints to the abstraction.
Dependencies are inferred from the claim text.