%T Working Towards the Agreement Problem Protocol Verification Environment
%A  James S. Pascoe,  Roger J. Loader,  Vaidy S. Sunderam
%E  Alan G. Chalmers,  Majid Mirmehdi,  Henk Muller
%B Communicating Process Architectures 2001
%X This paper proposes the Agreement Problem Protocol
   Verification Environment (APPROVE) for the automated formal
   verification of novel solutions to agreement problems in
   group communication systems. Agreement problems are
   characterized by the need for a group of processes to agree
   on a proposed value and are exemplified by group membership,
   consensus and fault\-tolerance scenarios. Due to their
   fundamental role, it is important that the correctness of
   new agreement algorithms be verified formally. In the past,
   the application of manual proof methods has been met with
   varying degrees of success, suggesting the need for a less
   error prone automated approach. An observation concerning
   previous proofs is that often a significant amount of effort
   is invested in modeling themes common to all such proofs,
   albeit using different formalisms. Thus, the APPROVE project
   aims to address these issues, its envisaged culmination
   being a usable software framework that exploits model
   re\-use wherever possible.