The sweep-line state space exploration method

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

The sweep-line method exploits intrinsic progress in concurrent systems to alleviate the state explosion problem in explicit state model checking. The concept of progress makes it possible to delete states from the memory during state space exploration and thereby reduce peak memory usage. The contribution of this paper is twofold. First, we provide a coherent presentation of the sweep-line theory and the many variants of the method that have been developed over the past 10 years since the basic idea of the method was conceived. Second, we survey a selection of case studies where the sweep-line method has been put into practical use for the verification of concurrent systems.
Original languageEnglish
JournalTheoretical Computer Science
Volume429
Pages (from-to)169–179
Number of pages11
ISSN0304-3975
DOIs
Publication statusPublished - 2012

See relations at Aarhus University Citationformats

ID: 48292088