@InProceedings{PascoeLoader01,
  title =        "{W}orking {T}owards the {A}greement {P}roblem {P}rotocol {V}erification {E}nvironment",
  author=        "Pascoe,  James S. and Loader,  Roger J. and Sunderam,  Vaidy S.",
  editor=        "Chalmers,  Alan G. and Mirmehdi,  Majid and Muller,  Henk",
  pages =        "213--230",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2001",
  isbn=          "1 58603 202 X",
  year=          "2001",
  month=         "sep",
  abstract=      "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."
}