The design of a linearization of a concurrent data object

The proof is made with the theorem prover NQTHM-1992 of Boyer and Moore, which can be obtained from nqthm-request@cli.com, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, Texas 78703, USA.

The algorithm, its design, and the construction of its proof are described in

The event files that can be read and submitted for NQTHM-1992 to yield a formal proof, at least of safety, are

Comments are welcome, September 29, 1998