The
SilVer tool
implements the
symbolic semantics 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.