Partial-order reduction for GPU model checking

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

9 Citations (Scopus)
2 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 explicitstate model checking, we improve memory efficiency by applying partialorder 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 publicationAutomated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings
PublisherSpringer
Pages357-374
Number of pages18
ISBN (Print)978-3-319-46519-7
DOIs
Publication statusPublished - 2016
Event14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 - Chiba, Japan
Duration: 17 Oct 201620 Oct 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume9938
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
Country/TerritoryJapan
CityChiba
Period17/10/1620/10/16

Fingerprint

Dive into the research topics of 'Partial-order reduction for GPU model checking'. Together they form a unique fingerprint.

Cite this