Scalable liveness verification

A computer program product increasing scalability in bounded liveness verification, the computer program product comprising:

• one or more computer readable storage media and program instructions stored on the one or more computer readable storage media, the program instructions comprising instructions to:
• receive, by one or more processors, a counterexample trace showing a bounded liveness failure and a set of parameters associated with the counterexample trace, wherein a counterexample trace refers to a finite length trace, and wherein bounded liveness refers to a group of traces;
• partition the counterexample trace into segments representing bound increments contributing to the bounded liveness failure;
• synthesize or otherwise modeling a bounded livelock with optionally one or more fairness constraints whose behavior is evaluated relative to received counterexample;
• identify a time interval in which the bounded livelock model indicates progress toward a bounded livelock failure with respect to the received counterexample trace;
• select a segment of the identified time interval which is compatible with one or more adjacent segments during which to repeat input values;
• evaluate, by one or more processors, the received counterexample after repeating the selected segment;
• determine, by one or more processors, whether the evaluation indicates that the counterexample falsifies a deeper bound with respect to a bound or an unbounded liveness counterexample;
• and
• responsive to determining the evaluation indicates that the counterexample falsifies a deeper bound, provide, by one or more processors, counterexample falsification results.

A computer system for ranking devices according to compatibility with a service, the computer program product comprising:

• one or more computer processors;
• one or more computer readable storage media;
• program instructions stored on the one or more computer readable storage media, the program instructions comprising instructions to:
• receive, by one or more processors, a counterexample trace showing a bounded liveness failure and a set of parameters associated with the counterexample trace, wherein a counterexample trace refers to a finite length trace, and wherein bounded liveness refers to a group of traces;
• partition the counterexample trace into segments representing bound increments contributing to the bounded liveness failure;
• synthesize or otherwise modeling a bounded livelock with optionally one or more fairness constraints whose behavior is evaluated relative to received counterexample;
• identify a time interval in which the bounded livelock model indicates progress toward a bounded livelock failure with respect to the received counterexample trace;
• select a segment of the identified time interval which is compatible with one or more adjacent segments during which to repeat input values;
• evaluate, by one or more processors, the received counterexample after repeating the selected segment;
• determine, by one or more processors, whether the evaluation indicates that the counterexample falsifies a deeper bound with respect to a bound or an unbounded liveness counterexample;
• and
• responsive to determining the evaluation indicates that the counterexample falsifies a deeper bound, provide, by one or more processors, counterexample falsification results.