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
- Theories for Mechanical Proofs of Imperative
programs, Formal Aspects of Computing 9 (1997) 448-468,
with the events files
while1.events,
linsearch.events,
weakfairness.events,
concprelude.events.
peterson.events.
- Invariants for the construction
of a handshake register, Information Processing
Letters 68 (1998) 173-177, with the events file
handshake.events.
-
An assertional criterion for atomicity, Acta Informatica
38 (2002) 343-366, with the events files
bloom.events and
vitanyi.events and
snapshot.events. These files need to import
concprelude.events.
- An assertional proof for a construction of an
atomic variable, with the events file
regvarHS.events
Comments are welcome, March 2004.