Combining Techniques to Reduce State Space and Prove Strong Properties

An on-the-fly symmetry reduction technique that exploits the lexicographic order on metarepresentations of Maude terms, and a technique that uses auxiliary data to verify strong properties that are not directly expressible in propositional temporal logic are presented. Both are implemented by simple transformations of rewrite theories. They are applied in the verification of a strong-consistency property of a client-server protocol, a simplification of the Chain-Replication protocol.