Patent ID: 9092569
Filing Date: 2015-07-28
Classification: G06F

Abstract:
1. 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, wherein the abstract traces comprise program traces generated as a result of abstract interpretation of the program P under an abstraction A, the abstraction A defining a method for over-approximating behaviors of the program P using a bounded representation, wherein the program P′ is generated responsive to determining that the abstraction A is not to be refined at least in one of the iterations of the enumerating, determining and computing.