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.

Mechanization of proofs and logical operations (msc 03B35), Distributed systems (msc 68M14), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Abstract data types; algebraic specification (msc 68Q65), Theorem proving (deduction, resolution, etc.) (msc 68T15), Symbolic computation and algebraic computation (msc 68W30)
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

van de Pol, J.C. (2001). A prover for the $ mu $ CRL toolset with applications : version 0.1. Software Engineering [SEN]. CWI.