In this paper, the authors study the verification of concurrent programs, such as lock-free implementations of stacks and queues in a runtime environment where garbage collection is absent.

For specifying the properties of these programs, the authors use automata parameterized on a finite set of variables and a data independence argument proposed by Wolper [1]. To express relationships between threads, they use invariants, which allow for a comparison of the states of two arbitrary threads. Other ideas such as predicate abstraction are also used in an extended way.

The paper presents experimental results that show the efficacy of the approach. The range of techniques used is impressive.