VERIFICATION OF CONCURRENT PROGRAMS: THE AUTOMATA-THEORETIC FRAMEWORK.

An automata-theoretic framework to the verification of concurrent and nondeterministic programs is presented. The basic idea is that to verify that a program P is correct, one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if the program P//A, which is obtained by combining P and A, terminates. This unifies previous works on verification of fair termination and verification of temporal properties.