Eternity variables to prove simulation of specifications

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