No Need to Be Stubborn: Partial-Order Reduction for GPU Model Checking Revisited

Rik van Spreuwel, Anton Wijs (Corresponderende auteur)

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

1 Citaat (Scopus)

Samenvatting

GPUexplore, a GPU-accelerated explicit-state LTL model checker, achieves significant speedups compared to sequential and multi-core CPU model checkers, but it is limited by the amount of memory available on GPUs. Partial-Order Reduction is a way to remedy this problem, by excluding unnecessary transitions and states from exploration. For this work, we implemented the ample and clustered-ample reduction techniques in GPUexplore. Experiments show that our implementations achieve reductions similar to the state-of-the-art Breadth-First Search configurations of multi-core LTSmin and sequential DiVinE and Spin without introducing significant computational overhead, even though LTSmin applies stubborn set reduction, which has often been reported as the most effective technique. At times, ample and cample reduction even speeds up exploration 4–100×.

Originele taal-2Engels
TitelLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification
Subtitel12th International Symposium, ISoLA 2024, Crete, Greece, October 27–31, 2024, Proceedings, Part III
RedacteurenTiziana Margaria, Bernhard Steffen
Plaats van productieCham
UitgeverijSpringer
Pagina's353-373
Aantal pagina's21
ISBN van elektronische versie978-3-031-75380-0
ISBN van geprinte versie978-3-031-75379-4
DOI's
StatusGepubliceerd - 30 okt. 2024
Evenement12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024 - Crete, Griekenland
Duur: 27 okt. 202431 okt. 2024

Publicatie series

NaamLecture Notes in Computer Science (LNCS)
Volume15221
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349

Congres

Congres12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024
Verkorte titelISoLA 2024
Land/RegioGriekenland
StadCrete
Periode27/10/2431/10/24

Vingerafdruk

Duik in de onderzoeksthema's van 'No Need to Be Stubborn: Partial-Order Reduction for GPU Model Checking Revisited'. Samen vormen ze een unieke vingerafdruk.

Citeer dit