System and method for verification of programs using threads having bounded lock chains

A system for model checking of concurrent multi-threaded programs with bounded lock chains, comprising:

• a memory storage device:
• and
• a model checking program stored in the memory storage device and executed by one or more processing cores, the model checking program being configured to analyze, using a processor, individual program threads in a concurrent multi-threaded program stored on memory storage media to determine sets of reachable states and lock access patterns for bounded lock chains, the model checking program being configured to track sets of states reachable from a given set of states and track lock acquisitions and releases by maintaining a bi-directional lock causality graph in the memory storage device;
• the model checking program is configured to use an acceptance condition of the lock causality graph to combine analysis results from multiple threads to determine whether there is a violation of a correctness property in the concurrent multi-threaded program, to reduce a reachability problem by taking a specialized cross product that removes pairs that are not reachable, and to keep projection automata separate to circumvent a state explosion problem and avoid construction of a global automata.