Multi-core SCC-Based LTL Model Checking

Vincent Bloemen, Jan Cornelis van de Pol

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

    9 Citations (Scopus)
    40 Downloads (Pure)

    Abstract

    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
    PublisherSpringer
    Pages18-33
    Number of pages16
    ISBN (Print)978-3-319-49051-9
    DOIs
    Publication statusPublished - Nov 2016

    Publication series

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

    Keywords

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

    Cite this

    Bloemen, V., & van de Pol, J. C. (2016). Multi-core SCC-Based LTL Model Checking. In R. Bloem, & E. Arbel (Eds.), Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016 (pp. 18-33). (Lecture Notes in Computer Science; Vol. 10028). Cham: Springer. https://doi.org/10.1007/978-3-319-49052-6_2