| CARVIEW |
Select Language
HTTP/2 301
date: Thu, 22 Jan 2026 10:56:21 GMT
content-type: text/html; charset=iso-8859-1
location: https://spinroot.com/swarm/
server: cloudflare
x-frame-options: SAMEORIGIN
content-security-policy: frame-ancestors 'self';
cf-cache-status: DYNAMIC
nel: {"report_to":"cf-nel","success_fraction":0.0,"max_age":604800}
report-to: {"group":"cf-nel","max_age":604800,"endpoints":[{"url":"https://a.nel.cloudflare.com/report/v4?s=wra8l6NI25cnVF0TUNy9A5smfCXfx7GmouCnD4CX71gtSwd499psfmlXmtVkAWtO%2BH9KVvGROGdER2p39hRzR3P5Z%2Bsmqp6TZEKDsw%3D%3D"}]}
cf-ray: 9c1e86308d4484ad-BOM
alt-svc: h3=":443"; ma=86400
HTTP/2 200
date: Thu, 22 Jan 2026 10:56:22 GMT
content-type: text/html
server: cloudflare
x-frame-options: SAMEORIGIN
content-security-policy: frame-ancestors 'self';
last-modified: Sun, 10 Mar 2019 21:02:48 GMT
report-to: {"group":"cf-nel","max_age":604800,"endpoints":[{"url":"https://a.nel.cloudflare.com/report/v4?s=kq9i4Jg11%2B8xIch63zo9VSThEytdgcHkzcF23s0iXn5%2BEEsD5vphAas60Ya0K4K2%2BM85m9MvbbAezMNpJt7dzqdInOZlbwq6%2BPOfpA%3D%3D"}]}
x-content-type-options: nosniff
x-xss-protection: 1; mode=block
cf-cache-status: DYNAMIC
nel: {"report_to":"cf-nel","success_fraction":0.0,"max_age":604800}
content-encoding: gzip
cf-ray: 9c1e86357f6084ad-BOM
alt-svc: h3=":443"; ma=86400
Swarm verification tool -- Version 3.2
| Swarm(1) | Swarm(1) |
NAME
- Swarm - verification script generator for Spin
SYNTAX
- swarm [config_file] [option]*
DESCRIPTION
-
Swarm generates a script that performs many small verification
jobs in parallel, that can increase the problem coverage
for very large verification problems by about an order of magnitude
compared to standard bitstate verification runs.
It is meant to be used on models for which standard verification
with exhaustive, bitstate, hash-compaction etc. either runs out of
memory, or takes more time than is available (e.g., days or weeks).
Swarm uses parallelism and search diversification to reach its objectives.
The user can use a configuration file to define how many processing cores are available, how much memory can be used, and how much time is maximally available, among a range of other optional parameter settings. Based on this information, swarm generates the script that runs as many independent jobs as possible in parallel, without exceeding any of the user-defined constraints. Swarm can run jobs using local CPU cores or remote machines in a grid network.
Swarm version is 3.2, from 5 June 2017, is an update that handles early stoppage better when more than one of the swarm workers has generated a trail files.
SOURCE
- GitHub/Swarm
(source, makefile, and a manual page with examples)
- Spin home page
- Spin source code
- Swarm 2.0:
- G.J. Holzmann, R. Joshi, A. Groce, Swarm Verification Techniques
IEEE Trans. on Software Engineering, Vol. 37, No. 6, Nov/Dec 2011, pp. 845-857.
- Swarm 1.0:
- --, Tackling large verification problems with the Swarm tool,
15th Spin Workshop, UCLA, Los Angeles, August 2008, LNCS 5156. - --, Swarm Verification,
Proc. ASE 2008, 23rd IEEE/ACM Int. Conf. on Automated Software Engineering, l'Aquila, Italy, Sept. 2008.
- Spin source code
You should have version 5.2.0 or later of Spin installed.
SEE ALSO
| spinroot homepage | last update: March 10, 2019 |