A prover for the $ mu $ CRL toolset with applications : version 0.1

This document describes an automated theorem prover, based on an extension of binary decision diagrams. The prover transforms quantifier-free formulae into equivalent BDD-forms, w.r.t.~to some algebraic data specification. The prover is used by four tools for the symbolic analysis of distributed systems specified in $mu$CRL (i.e.~process algebra plus algebraic data types). The main techniques are invariants and confluence. Two case studies are reported: the DKR leader election protocol [13], and SPLICE [15], a coordination architecture of industrial origin. In both cases using confluence information leads to a reduced state space.