SLiVER is a tool for the analysis of multi-agent systems specified in the LAbS language [1]. At the moment, it support under-approximate analysis via bounded model checking, or analysis of the full state space via explicit-state model checking.
This page contains source code and binary releases of SLiVER for Linux x64 systems.
Typically, a SLiVER release will contain the following files and directories:
| Filename | Description |
|---|---|
examples/ |
Example LAbS specifications |
HISTORY |
Change log |
README.md |
This document |
README.txt |
Release-specific instructions |
requirements.txt |
Python dependencies |
sliver.py |
SLiVER command-line front-end |
sliver/ |
SLiVER code |
*.py |
SLiVER support files |
| other files and directories | Python libraries used by SLiVER |
To install SLiVER, please follow the steps below:
-
Install Python 3.10 or higher.
-
(Optional) Install Python 2.7 (required by the bundled CSeq backend).
-
Download and extract the latest version of SLiVER from the Releases page
-
Set execution (+x) permissions for
sliver.py,cseq/cseq.py,cbmc-simulator -
Install dependencies with
pip install -r requirements.txt -
Invoking
./sliver.py --helpfrom the command line should now display basic usage directions. -
Follow
README.txtfor additional (release-specific) instructions.
The COORDINATION paper [3] (PDF) contains further usage information.
If you encounter any issues while running SLiVER, please submit an issue.
R. De Nicola, L. Di Stefano, and O. Inverso, “Multi-Agent Systems with Virtual Stigmergy,” in Software Technologies: Applications and Foundations (STAF) Workshops. LNCS, vol 11176. Springer, 2018. Link
R. De Nicola, L. Di Stefano, and O. Inverso, “Multi-agent systems with virtual stigmergy,” Sci. Comput. Program., vol. 187, p. 102345, 2020. Link
R. De Nicola, L. Di Stefano, O. Inverso, and S. Valiani, “Modelling Flocks of Birds from the Bottom Up”, in 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), LNCS, vol. 13703. Springer, 2022. Link
R. De Nicola, L. Di Stefano, O. Inverso, and S. Valiani, “Process algebras and flocks of birds”, in A journey from process algebra via timed automata to model learning - Essays dedicated to Frits Vaandrager on the occasion of his 60th birthday. LNCS, vol. 13560. Springer, 2022. Link
L. Di Stefano, “Modelling and Verification of Multi-Agent Systems via Sequential Emulation,” PhD Thesis, Gran Sasso Science Institute, L’Aquila, Italy, 2020. Link
L. Di Stefano, F. Lang, and W. Serwe, “Combining SLiVER with CADP to Analyze Multi-agent Systems,” in 22nd International Conference on Coordination Models and Languages (COORDINATION). LNCS, vol. 12134. Springer, 2020. Link
L. Di Stefano and F. Lang, “Verifying temporal properties of stigmergic collective systems using CADP,” in 10th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), LNCS, vol. 13036. Springer, 2021. Link
L. Di Stefano and F. Lang, “Compositional Verification of Stigmergic Collective Systems”, in 24th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 13881. Springer, 2023. Link