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 language | English |
---|---|
Title of host publication | Automated Technology for Verification and Analysis |
Subtitle of host publication | 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings |
Editors | Cyrille Artho, Axel Legay, Doron Peled |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 357-374 |
Number of pages | 18 |
ISBN (Electronic) | 978-3-319-46520-3 |
ISBN (Print) | 978-3-319-46519-7 |
DOIs | |
Publication status | Published - Oct 2016 |
Event | 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 - Chiba, Japan Duration: 17 Oct 2016 → 20 Oct 2016 Conference number: 14 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Verlag |
Volume | 9938 |
ISSN (Print) | 0302-9743 |
Conference
Conference | 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 |
---|---|
Abbreviated title | ATVA |
Country/Territory | Japan |
City | Chiba |
Period | 17/10/16 → 20/10/16 |
Keywords
- CR-D.2.4
- FMT-MC: MODEL CHECKING
- n/a OA procedure