DYNAMIC SYNTHESIS OF PROGRAM SYNCHRONIZATION

专利名称：DYNAMIC SYNTHESIS OF PROGRAM

SYNCHRONIZATION

发明人：Martin Vechev,Eran Yahav申请号：US13560548申请日：20120727

公开号：US20130247001A1公开日：20130919

专利附图：

摘要：Dynamic synthesis includes receiving a program P and a specification S thatdescribes desired properties of P. The dynamic synthesis also includes initializing aconstraint C to true, enumerating schedules up to a defined limit that satisfy C, and

executing a schedule of P. The dynamic synthesis further includes determining whetherexecution of the schedule violates S. In response to determining that the executionviolates S, the dynamic synthesis includes determining whether to avoid future executionsof the schedule. In response to determining that future executions of the scheduleshould be avoided, the dynamic synthesis includes computing a constraint that avoids thefuture execution, and adding the constraint to C; otherwise, the dynamic synthesisincludes selecting another schedule for execution. In response to determining that theexecution of the schedule does not violate S, the dynamic synthesis includes selectinganother schedule for execution.

申请人：Martin Vechev,Eran Yahav

地址：Zurich CH,Haifa IL

国籍：CH,IL

更多信息请下载全文后查看