Partial-Order Reduction for GPU Model Checking

Thomas Neele*, A. Wijs, Dragan Bošnački, Jaco van de Pol

*Corresponding author for this work

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

12 Citations (Scopus)
95 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 languageEnglish
Title of host publication Automated Technology for Verification and Analysis
Subtitle of host publication14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings
EditorsCyrille Artho, Axel Legay, Doron Peled
Place of PublicationBerlin
PublisherSpringer
Pages357-374
Number of pages18
ISBN (Electronic)978-3-319-46520-3
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
Country/TerritoryJapan
CityChiba
Period17/10/1620/10/16

Keywords

  • CR-D.2.4
  • FMT-MC: MODEL CHECKING
  • n/a OA procedure

Fingerprint

Dive into the research topics of 'Partial-Order Reduction for GPU Model Checking'. Together they form a unique fingerprint.

Cite this