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, is a reimplementation of the algorithm, making more extensive use of search randomization techniques, and taking advantage of some new features implemented for this purpose in Spin Version 5.2 and later.

SOURCE

    swarm3.1.tar 8 April 2011, (source, makefile, and a manual page with examples)
    N.B. This version of Swarm assumes that you have version 5.2.0 of Spin or later (executable, source).

BUGS

    [email protected]

SEE ALSO

  • Spin home page
  • Swarm Version 2 and 3:
    • G.J. Holzmann, R. Joshi, A. Groce, Swarm Verification Techniques -- to appear.
  • Swarm Version 1:
    • --, 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: April 9, 2011