Patent Document ID: 20160147640
Application ID: 14553056
Patent Status: 0

Claim One:
1. A system comprising: at least one processor; a constraint solver executable by the at least one processor; non-transitory computer-readable medium storing instructions executable by the at least one processor to maximize detection of concurrency bugs in a multithreaded software program (“program”), the instructions executable by the at least one processor to: formulate detection as a constraint-solving problem by: assigning an order variable to each of a plurality of events in an input trace of the program; ordering the order variables to corresponding events in an order of execution according to a maximal causal model, which captures a set of feasible traces that can be generated by a multithreaded program capable of generating the input trace; and generating a formula over the plurality of order variables and over a plurality of branch variables corresponding to branch events that captures the maximal causal model, control flow, and a trace property whose violation corresponds to a concurrency bug; and solve the formula with a constraint solver to determine whether the property is violated due to the concurrency bug.