Verification of concurrent systems in SML

There can be different views of a concurrent, distributed system, depending on who observes it. The final user may just want to know how the system behaves in terms of its possible sequences of actions, while the designer wants to know which are the sequential components of a system or how it is distributed in space. Moreover, there is no widely accepted semantic model for concurrent systems. In this paper we describe the use of the SML language in the implementation of a parametric verification tool for process description languages. It allows symbolic execution of processes at different levels, and provides facilities for equivalence checking.