Partial-Order Reduction for GPU Model Checking

T. Neele, A. Wijs, D. Bosnacki, Jan Cornelis van de Pol

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

    7 Citations (Scopus)
    48 Downloads (Pure)

    Abstract

    Model checking using GPUs has seen increased popularity over the last years. Because GPUs have a limited amount of memory, only small to medium-sized systems can be verified. For on-the-fly explicit-state model checking, we improve memory efficiency by applying partial-order reduction. We propose novel parallel algorithms for three practical approaches to partial-order reduction. Correctness of the algorithms is proved using a new, weaker version of the cycle proviso. Benchmarks show that our implementation achieves a reduction similar to or better than the state-of-the-art techniques for CPUs, while the amount of runtime overhead is acceptable.
    Original languageUndefined
    Title of host publicationProceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
    EditorsC Artho, A. Legay, D. Peled
    Place of PublicationBerlin
    PublisherSpringer
    Pages357-374
    Number of pages18
    ISBN (Print)978-3-319-46519-7
    DOIs
    Publication statusPublished - Oct 2016
    Event14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 - Chiba, Japan
    Duration: 17 Oct 201620 Oct 2016
    Conference number: 14

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume9938
    ISSN (Print)0302-9743

    Conference

    Conference14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
    Abbreviated titleATVA
    CountryJapan
    CityChiba
    Period17/10/1620/10/16

    Keywords

    • CR-D.2.4
    • EWI-27826
    • FMT-MC: MODEL CHECKING

    Cite this

    Neele, T., Wijs, A., Bosnacki, D., & van de Pol, J. C. (2016). Partial-Order Reduction for GPU Model Checking. In C. Artho, A. Legay, & D. Peled (Eds.), Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 (pp. 357-374). (Lecture Notes in Computer Science; Vol. 9938). Berlin: Springer. https://doi.org/10.1007/978-3-319-46520-3_23