A. Prasad Sistla, Moshe Y. Vardi, et al.
Theoretical Computer Science
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.
A. Prasad Sistla, Moshe Y. Vardi, et al.
Theoretical Computer Science
Joseph Y. Halpern, Moshe Y. Vardi
Journal of Computer and System Sciences
Joseph Y. Halpern, Moshe Y. Vardi
STOC 1988
Moshe Y. Vardi
Information Processing Letters