Patent ID: 8266600

Claim:
A method for model checking of a concurrent multi-threaded software program for a correctness property, said method comprising computer implemented steps of: modeling the multi-threaded software program as a concurrent system of pushdown systems communicating using nested locks, each thread modeled as a pushdown system; analyzing each individual thread of the program such that each lock is associated, between the lock's acquisition and release, with a separate set of backward and forward lock acquisition histories, where a backward lock acquisition history for a given lock is the set of only the locks that have been released before the given lock is released, and a forward lock acquisition history for the given lock is the set of only the locks that have been acquired after the given lock is acquired; and merging analysis results by checking compatibility of lock acquisition histories from a plurality of said individual threads to determine whether the program satisfies the correctness property, expressed as a temporal logic formula.