Using pushdown systems for the static analysis of multi-threaded programs

A computer-implemented method of soundly analyzing a concurrent multi-threaded computer program for correctness properties specified as Linear Temporal Logic formulae using Lock Constrained Multi-Automata Pairs wherein said multi-threaded computer program comprises multiple threads wherein one or more of said multiple threads synchronize and communicate with one or more of other ones of said multiple threads and wherein said multi-threaded computer program has a set of locations of interest which pertain to a particular property of interest that refers to more than one thread, said method comprising steps of:

• by the computer:
• augmenting states of the individual threads with backward and forward acquisition history information;
• determining a set of reachable states augmented with backward and forward acquisition history information in each one of the individual augmented threads by traversing the individual threads to compute augmented Multi-Automata that store these acquisition histories for all reachable states in threads;
• and
• determining simultaneous reachability of certain states in the concurrent program as required by the structure of the temporal logic formula by building a Lock Constrained Multi-automata pair from the augmented Multi-automata computed in the previous step and encoding reachability as a consistency check on the backward and forward acquisition histories as stored in the local states of the augmented Multi-automata.