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
firstname.lastname@example.org, Computational Logic, Inc.,
1717 West Sixth Street, Suite 290,
Austin, Texas 78703, USA.
The material is explained in
Comments are welcome, March 2004.
- Theories for Mechanical Proofs of Imperative
programs, Formal Aspects of Computing 9 (1997) 448-468,
with the events files
- Invariants for the construction
of a handshake register, Information Processing
Letters 68 (1998) 173-177, with the events file
An assertional criterion for atomicity, Acta Informatica
38 (2002) 343-366, with the events files
snapshot.events. These files need to import
- An assertional proof for a construction of an
atomic variable, with the events file