Informed swarm verification of infinite-state systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic


Swarm verification and parallel randomised depth-first search are very effective parallel techniques to hunt bugs in large explicit state spaces. In case bugs are absent, however, scalability of the parallelisation is completely lost. Informed swarm verification is an extension, in which workers periodically communicate with a manager to perform bounded searches. The workers do not synchronise with each other, though. This scheme helps each worker to perform a finite search, even if the state space is infinitely large, while still benefitting from randomisation to find bugs quickly. Because the workers operate independently, this technique is very suitable for large-scale parallel explicit state space exploration on a computer cluster. A prototype of this technique has been implemented in the LTSmin toolset, developed at the University of Twente.
Original languageEnglish
Title of host publicationProceedings of the 13th International Workshop on Verification of Infinite-State Systems, October 10, 2011, Taipei, Taiwan
Place of PublicationSydney
PublisherOpen Publishing Association
Publication statusPublished - 2011

Publication series

NameElectronic Proceedings in Theoretical Computer Science
ISSN (Print)2075-2180


Dive into the research topics of 'Informed swarm verification of infinite-state systems'. Together they form a unique fingerprint.

Cite this