Issue No.09 - September (1990 vol.16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.58787
<p>A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree.</p>
mechanically verifying concurrent programs; Boyer-Moore prover; proof system; Unity; safety; liveness; operational semantics; transition system model; concurrency; inference rules; encoding; distributed algorithm; encoding; inference mechanisms; parallel programming; program verification; theorem proving.
D.M. Goldschlag, "Mechanically Verifying Concurrent Programs with the Boyer-Moore Prove", IEEE Transactions on Software Engineering, vol.16, no. 9, pp. 1005-1023, September 1990, doi:10.1109/32.58787