Abstraction-guided synthesis

A computer readable storage medium storing a program of instructions executable by a machine to perform 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.

A system for abstraction-guided synthesis, comprising:

• a memory device operable to store 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;
• and
• a processor operable to initialize constraint C to true, enumerate abstract traces of the program P that satisfy the constraint C and determine whether there is a trace in the abstract traces violating the specification S,
• the processor in response to determining that there is a trace that violates the specification S, further operable to select a trace T that violates the specification S, determine whether to refine the abstraction A,
• the processor in response to determining to refine the abstraction A, further operable to refine the abstraction A to avoid the trace T that violates the specification S, and set the abstraction A to be the refined abstraction,
• the processor in response to determining that the abstraction A should not be refined, further operable to compute one or more constraints that avoid the trace T that violates the specification S, and add the constraint to the constraint C;
• the processor further operable to repeat the enumeration of abstract traces and computing of one or more constraints;
• and
• the processor in response to determining that there is no trace that violates the specification S, further operable to generate program P′ that modifies the program P by including one or more constraints specified in the constraint C.

A method for abstraction-guided synthesis, comprising:

• enumerating abstract traces of a program P;
• determining, using a processor, a trace in the abstract traces violating a specification S that describes the program P;
• computing one or more constraints that avoid the trace T that violates the specification S, and adding the constraint to constraint C;
• repeating the steps of enumerating, determining and computing;
• 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.