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, is an update that handles early stoppage better when more than one of the swarm workers has generated a trail files.

SOURCE

    swarm3.2.tar.gz 5 June 2017, (source, makefile, and a manual page with examples)
    N.B. This version of Swarm assumes that you have version 5.2.0 or later of Spin installed (executable, source).

BUGS

SEE ALSO

  • Spin home page
  • 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: June 5, 2017