This theory is developed in the paper Eternity Variables to Prove Simulation of Specifications ACM-ToCL 6 (2005) 1-27. Almost all of it has been verified with a proof script for the theorem prover PVS.

The theory is applied to the serializable database
interface problem of Distributed Computing 6 (1992). This work is
described in

Eternity variables to specify and prove a serializable database
interface, Science of Computer Programming
** 51** (2004) 47--85.

The mechanical
proof was done with
NQTHM, based on my
prelude for concurrency.

The completeness result has been simplified and extended in
Universal extensions to simulate specifications,
Information and Computation **206** (2008) 108-128.
This has been verified with a
proof script in PVS.

A simpler application of eternity variables as well as the development of gliding simulations is in the paper A Criterion for Atomicity Revisited. The PVS proof script has been revised (Oct. 2007) to accomodate the next application.

This revised criterion for atomicity has been applied to prove
algorithm C2 of Haldar and Vidyasankar in
A challenge for atomicity verification, Science of Computer
Programming **71** (2008) 57-72, with refinement functions and
forward simulations, and
verified with PVS.

In "Simulation refinement for concurrency verification" (2009) we introduced episodic simulations with application to Lipton's mutual exclusion theory and mutex abstraction in (e.g.) pthreads. This is also verified with PVS.

Comments and questions are welcome.

Last modified: Fri Apr 24 10:41:39 CEST 2009

Wim H. Hesselink, e-mail: w.h.hesselink@rug.nl