Multi-core SCC-Based LTL Model Checking

Vincent Bloemen, Jan Cornelis van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    11 Citations (Scopus)
    43 Downloads (Pure)


    We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel. To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.
    Original languageUndefined
    Title of host publicationHardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016
    EditorsRoderick Bloem, Eli Arbel
    Place of PublicationCham
    Number of pages16
    ISBN (Print)978-3-319-49051-9
    Publication statusPublished - Nov 2016

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer International Publishing
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    • METIS-320900
    • IR-102924
    • Model Checking
    • Multi-Core
    • SCC
    • accepting cycle
    • LTL
    • strongly connected component
    • EWI-27453

    Cite this