A Mechanization of Unity in PC-NQTHM-92

This paper presents in detail how the Unity logic for reasoning about concurrent programs was formalized within the mechanized theorem prover PC-NQTHM-92. Most of Unitys proof rules were formalized in the unquantified logic of NQTHM, and the proof system has been used to mechanically verify several concurrent programs. The mechanized proof system is sound by construction, since Unitys proof rules were proved about an operational semantics of concurrency, also presented here. Skolem functions are used instead of quantifiers, and the paper describes how proof rules containing Skolem function are used instead of Unitys quantified proof rules when verifying concurrent programs. This formalization includes several natural extensions to Unity, including nondeterministic statements. The paper concludes with a discussion of the cost and value of mechanization.