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 , and SPLICE , 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]|
|Organisation||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.