TY - GEN
T1 - Partial-order reduction for GPU model checking
AU - Neele, T.S.
AU - Wijs, A.J.
AU - Bošnački, D.
AU - van de Pol, J.C.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84992493173&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-46520-3_23
DO - 10.1007/978-3-319-46520-3_23
M3 - Conference contribution
AN - SCOPUS:84992493173
SN - 978-3-319-46519-7
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 357
EP - 374
BT - Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings
PB - Springer
T2 - 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
Y2 - 17 October 2016 through 20 October 2016
ER -