NQTHM proving imperative programs

This directory contains some files to show that the theorem prover NQTHM-1992 of Boyer and Moore can be used to prove imperative programs like linear search, Peterson's algorithm for mutual exclusion of two processes, and Bloom's atomic register for two writers. This theorem prover can be obtained from nqthm-request@cli.com, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, Texas 78703, USA.

The material is explained in

Comments are welcome, March 2004.