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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/91/1370/CS-TR-91-1370.pdf