Patent ID: 9678853
Date: 2017-06-13
CPC Classifications: G06F

Claim:
1. A method for mapping a bounded liveness failure to a concrete counterexample of a liveness property of a system component, the method comprising: receiving, by one or more processors, a trace of a bounded liveness failure of a system component, a set of fairness constraints and continuous liveness assertion conditions corresponding to the trace; generating, by one or more processors, randomized values for one or more unassigned input values of one or more registers of the trace and for unassigned register values of the one or more registers of the trace; simulating, by one or more processors, traversal of each state of a sequence of states of the trace; determining, by one or more processors, whether a repetition of a state of the sequence of states of the trace is produced by traversing the sequence of states of the trace; and responsive to determining that traversing the sequence of states of the trace does result in a repetition of a state of the sequence of states of the trace, and determining that the set of fairness constraints are asserted within the sequence of states leading to the repetition of a state of the sequence of states, and that the continuous liveness assertion conditions are maintained throughout the sequence of states leading to the repetition of the state of the sequence of states, reporting, by one or more processors, a concrete counterexample of a liveness property of the system component.