Verification of concurrent programs: the automata-theoretic framework^* * A prelimary version of this paper appeared in Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca, 1987, pp. 167-176.

Abstract

Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 (1991) 79-98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. 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 a program PA, obtained by combining P and A, terminates. We formalize this idea in a framework of ω-automata with a recursive set of states. This unifies previous works on verification of fair termination and verification of temporal properties. © 1991.