分散コンピューティング環境におけるソフトウェアの解析の効率的な並列化のためのノードの計算の初期化手法

摘要

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.