Swarm(1)Swarm(1)

NAME

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)
    You should have version 5.2.0 or later of Spin installed.

    SEE ALSO

    • 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.
    spinroot homepage last update: March 10, 2019