Partial-Order Reduction for GPU Model Checking

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

  • 3 Citations

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 languageUndefined
Title of host publicationProceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
EditorsC Artho, A. Legay, D. Peled
Place of PublicationBerlin
PublisherSpringer Verlag
Pages357-374
Number of pages18
ISBN (Print)978-3-319-46519-7
DOIs
StatePublished - Oct 2016
Event14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 - Chiba, Japan

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
CountryJapan
CityChiba
Period17/10/1620/10/16

Fingerprint

Model checking
Parallel algorithms
Program processors

Keywords

  • CR-D.2.4
  • EWI-27826
  • FMT-MC: MODEL CHECKING

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). Berlin: Springer Verlag. DOI: 10.1007/978-3-319-46520-3_23

Neele, T.; Wijs, A.; Bosnacki, D.; van de Pol, Jan Cornelis / Partial-Order Reduction for GPU Model Checking.

Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016. ed. / C Artho; A. Legay; D. Peled. Berlin : Springer Verlag, 2016. p. 357-374 (Lecture Notes in Computer Science; Vol. 9938).

Research output: Scientific - peer-reviewConference contribution

@inbook{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 = "10",
doi = "10.1007/978-3-319-46520-3_23",
isbn = "978-3-319-46519-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
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",

}

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 Verlag, Berlin, pp. 357-374, 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, Chiba, Japan, 17-20 October. DOI: 10.1007/978-3-319-46520-3_23

Partial-Order Reduction for GPU Model Checking. / Neele, T.; Wijs, A.; Bosnacki, D.; van de Pol, Jan Cornelis.

Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016. ed. / C Artho; A. Legay; D. Peled. Berlin : Springer Verlag, 2016. p. 357-374 (Lecture Notes in Computer Science; Vol. 9938).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Partial-Order Reduction for GPU Model Checking

AU - Neele,T.

AU - Wijs,A.

AU - Bosnacki,D.

AU - van de Pol,Jan Cornelis

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

PB - Springer Verlag

ER -

Neele T, Wijs A, Bosnacki D, van de Pol JC. Partial-Order Reduction for GPU Model Checking. In Artho C, Legay A, Peled D, editors, Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016. Berlin: Springer Verlag. 2016. p. 357-374. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-46520-3_23