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

1. 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.

2. The method of claim 1 further comprising the steps of by the computer:

simplifying the given property into its set of basic operators;

analyzing the multi-threaded program for each individual operator thereby producing a set of analysis results; and

combining the results into a set of results for the original property.

3. The method of claim 2 further comprising the step of by the computer checking consistency over states in pairs of automata for each basic operator.

4. The method of claim 1 wherein the states in a thread and/or a property are augmented by the computer depending on the synchronization and communication primitives and the original property.

5. The method of claim 4 wherein threads are augmented by the computer with acquisition histories when locks are used as the primitives for synchronization and communication.

6. The method of claim 5 wherein said acquisition history includes both forward acquisition history and backward acquisition history of the locks.