We describe a mechanical proof system for concurrent programs, based on a formalization of the temporal framework of Manna and Pnueli as an extension of the computational logic of Boyer and Moore. The system provides a natural representation of specifications of concurrent programs as temporal logic formulas, which are automatically translated into terms that are subject to verification by the Boyer-Moore prover. Several specialized derived rules of inference are introduced to the prover in order to facilitate the verification of invariance (safety) and eventuality (liveness) properties. The utility of the system is illustrated by a correctness proof for a two-process program that computes binomial coefficients.
Full paper: ps, pdf (appeared in Formal Aspects of Computing 4: 597-611, 1992)