Patent ID: 8763001

Claim:
A distributed computing system, comprising: two or more worker nodes, the worker nodes configured to execute a job comprising a portion of code to be verified; and a scheduler node comprising a processor coupled to a memory, wherein: the memory comprises: a resource queue indicating a plurality of worker nodes available to verify a portion of code; and a job queue indicating one or more jobs to be executed by a worker node, each job indicating a portion of a code to be verified; based on a determination by the scheduler node that both the resource queue and the job queue contain entries, the scheduler node is configured to: apply a scheduling policy to select a first job; select a first worker node as a best match for the characteristics of the first job among the resource queue entries; wherein: the best match includes a lowest initialization cost for the first job among the worker nodes in the resource queue; determining initialization cost of the worker node for the first job includes determining: a common prefix between an initialization path condition of the first job and a termination path condition of the worker node; backtracking steps from the termination path condition to reach the common prefix; forward steps to reach an initial path condition; and costs of the backtracking steps and the forward steps; assign the first job to the first worker node; assign first parameters to the first worker node based on a job creation policy, the first parameters indicating first criteria for evaluation by the first worker node, the first criteria specifying when the first worker node, after being assigned the first job, will define a new job; and assign second parameters to the first worker node based on a termination policy for halting execution of the first job, the second parameters indicating second criteria for evaluation by the first worker node.