Reseña: A framework for formally verifying software transactional memory algorithms

Se ha publicado un nuevo artículo de verificación con PVS:
A framework for formally verifying software transactional memory algorithms que se presentará el 3 de Septiembre en CONCUR 2012 (23rd International Conference on Concurrency Theory).

Sus autores son Mohsen Lesani, Victor Luchangco y Mark Moir. El primero trabaja en UCLA y los restantes en Oracle.

El resumen del artículo es

We present a framework for verifying transactional memory (TM) algorithms. Specifications and algorithms are specified using I/O automata, enabling hierarchical proofs that the algorithms implement the specifications. We have used this framework to develop what we believe is the first fully formal machine-checked verification of a practical TM algorithm: the NOrec algorithm of Dalessandro, Spear and Scott.

Our framework is available for others to use and extend. New proofs can leverage existing ones, eliminating significant work and complexity.