An Incremental Stuttering Renement Proof of a Concurrent Program in ACL2

We present an incremental renement proof in ACL2 which demonstrates the reduction of the observable behaviors of a concurrent program to those of a much simpler program. In particular, we document the proof of correctness of a concurrent program which implements the operations of a double-ended queue in the application of a work-stealing algorithm. The demonstration is carried out by proving a renement from the implementation to a specication via an intermediate model. We document the use of the intermediate model in dividing the veri cation problem into more manageable steps which in turn allow for more eective proof reductions in ACL2. In both steps, the more abstract system is allowed nite stuttering and this is important in correlating renement proof with progress in the more concrete system.