We investigate and improve the scalability of multi-core LTL model checking. Our algorithm, based on parallel DFS-like SCC decomposition, is able to efficiently decompose large SCCs on-the-fly, which is a difficult problem to solve in parallel.
To validate the algorithm we performed experiments on a 64-core machine. We used an extensive set of well-known benchmark collections obtained from the BEEM database and the Model Checking Contest. We show that the algorithm is competitive with the current state-of-the-art model checking algorithms. For larger models we observe that our algorithm outperforms the competitors. We investigate how graph characteristics relate to and pose limitations on the achieved speedups.
|Title of host publication||Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016|
|Editors||Roderick Bloem, Eli Arbel|
|Place of Publication||Cham|
|Number of pages||16|
|Publication status||Published - Nov 2016|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer International Publishing|
- Model Checking
- accepting cycle
- strongly connected component