Report Number: CS-TR-91-1370
Institution: Stanford University, Department of Computer Science
Title: An NQTHM mechanization of "An Exercise in the Verification of Multi-Process Programs"
Author: Nagayama, Misao
Author: Talcott, Carolyn
Date: June 1991
Abstract: This report presents a formal verification of the local correctness of a mutex algorithm using the Boyer-Moore theorem prover. The formalization follows closely an informal proof of Manna and Pnuelli. The proof method of Manna and Pnueli is to first extract from the program a set of states and induced transition system. One then proves suitable invariants. There are two variants of the proof. In the first (atomic) variant, compound tests involving quantification over a finite set are viewed as atomic operations. In the second (molecular) variant, this assumption is removed, making the details of the transitions and proof somewhat more complicated. The original Manna-Pnueli proof was formulated in terms of finite sets. This led to concise and elegant informal proof, however one that is not easy to mechanize in the Boyer-Moore logic. In the mechanized version we use a dual isomorphic representation of program states based on finite sequences. Our approach was to outline the formal proof of each invariant, making explicit the case analyses, assumptions and properties of operations used. The outline served as our guide in developing the formal proof. The resulting sequence of events follows the informal plan quite closely. The main difficulties encountered were in discovering the precise form of the lemmas and hints necess to guide the theorem prover.