of the link-calculus. The SilVer tool takes as input a link-calculus model and outputs the graph of the labelled transition system of the model. It exploits an abstraction technique that allows for a more efficient execution of the semantics of the calculus. In fact, unlike the operational semantics of the link-calculus, the symbolic semantics is finitely branching and it represents, compactly, a possibly infinite number of transitions.
The tool offers the possibility to test for network bisimilarity and verifying whether a process satisfies a formula in the symbolic link modal logic The new version of the tool is provided with a friendly graphical interface.