Partial-Order Reduction for GPU Model Checking

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

doi:10.1007/978-3-319-46520-3_23

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 proceeding › Conference contribution › Academic › peer-review

9 Citations (Scopus)

84 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 language	Undefined
Title of host publication	Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
Editors	C Artho, A. Legay, D. Peled
Place of Publication	Berlin
Publisher	Springer
Pages	357-374
Number of pages	18
ISBN (Print)	978-3-319-46519-7
DOIs	https://doi.org/10.1007/978-3-319-46520-3_23
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
EWI-27826
FMT-MC: MODEL CHECKING

Access to Document

10.1007/978-3-319-46520-3_23

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). Springer. https://doi.org/10.1007/978-3-319-46520-3_23

@inproceedings{a5313dd392a7456a9c4348aaacada0a9,

title = "Partial-Order Reduction for GPU Model Checking",

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.",

keywords = "CR-D.2.4, EWI-27826, FMT-MC: MODEL CHECKING",

author = "T. Neele and A. Wijs and D. Bosnacki and {van de Pol}, {Jan Cornelis}",

year = "2016",

month = oct,

doi = "10.1007/978-3-319-46520-3_23",

language = "Undefined",

isbn = "978-3-319-46519-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "357--374",

editor = "C Artho and A. Legay and D. Peled",

booktitle = "Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016",

note = "14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 ; Conference date: 17-10-2016 Through 20-10-2016",

}

Neele, T, Wijs, A, Bosnacki, D & van de Pol, JC 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. Lecture Notes in Computer Science, vol. 9938, Springer, Berlin, pp. 357-374, 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, Chiba, Japan, 17/10/16. https://doi.org/10.1007/978-3-319-46520-3_23

Partial-Order Reduction for GPU Model Checking. / Neele, T.; Wijs, A.; Bosnacki, D. et al.
Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016. ed. / C Artho; A. Legay; D. Peled. Berlin: Springer, 2016. p. 357-374 (Lecture Notes in Computer Science; Vol. 9938).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Partial-Order Reduction for GPU Model Checking

AU - Neele, T.

AU - Wijs, A.

AU - Bosnacki, D.

AU - van de Pol, Jan Cornelis

N1 - Conference code: 14

PY - 2016/10

Y1 - 2016/10

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 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.

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 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.

KW - CR-D.2.4

KW - EWI-27826

KW - FMT-MC: MODEL CHECKING

U2 - 10.1007/978-3-319-46520-3_23

DO - 10.1007/978-3-319-46520-3_23

M3 - Conference contribution

SN - 978-3-319-46519-7

T3 - Lecture Notes in Computer Science

SP - 357

EP - 374

BT - Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016

A2 - Artho, C

A2 - Legay, A.

A2 - Peled, D.

PB - Springer

CY - Berlin

T2 - 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016

Y2 - 17 October 2016 through 20 October 2016

ER -