Patent ID: 8495588

Claim:
A method for abstraction-guided synthesis, comprising: receiving a program P, a specification S that describes desired properties of the program P, an abstraction A that defines a method for over-approximating behaviors of the program P using a bounded representation; initializing constraint C to true; enumerating abstract traces of the program P that satisfy the constraint C; determining, using a processor, whether there is a trace in the abstract traces violating the specification S; in response to determining that there is a trace that violates the specification S, selecting a trace T that violates the specification S; determining whether to refine the abstraction A; in response to determining to refine the abstraction A, refining abstraction A to avoid the trace T that violates the specification S, and setting the abstraction A to be the refined abstraction; in response to determining that the abstraction A should not be refined, computing one or more constraints that avoid the trace T that violates the specification S, and adding the constraint to the constraint C; returning to the step of enumerating and repeating the step of determining; and in response to determining that there is no trace that violates the specification S, generating program P′ that modifies the program P by including one or more constraints specified in the constraint C.