Node computation initialization technique for efficient parallelization of software analysis in a distributed computing environment

摘要

A method for verifying software includes determining an initialization path condition of a received software verification job, determining a termination path condition of a computing node, and initializing the execution of the received software verification job on the computing node based on the initialization path condition and the termination path condition. The initialization path condition includes a sequence of program predicates for reaching a starting state of software to be verified. The received software verification job includes an indication of a portion of the software to be verified. The termination path condition includes an indication of the last state reached during the execution of a previous software verification job on the computing node. The computing node is assigned to execute the received software verification job.

主权项

1. A method for verifying software, comprising:
determining an initialization path condition of a received software verification job, wherein: the initialization path condition comprises a sequence of program predicates for reaching a starting state of software to be verified; and the received software verification job comprises an indication of a portion of the software to be verified; determining a termination path condition of a computing node, the termination path condition comprising an indication of the last state reached during the execution of a previous software verification job on the computing node, the computing node assigned to execute the received software verification job; and initializing the execution of the received software verification job on the computing node based on the initialization path condition and the termination path condition; wherein initializing the execution of the received software verification job utilizes a backtrack-and-replay technique, the backtrack-and-replay technique comprising:
beginning with the termination path condition, backtracking the predicate steps taken to reach the termination path condition until the path condition is equivalent to a prefix of the initialization path condition; andbeginning at the prefix, replaying the remaining predicate steps of the initialization path condition until the initialization path condition is reached.