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.
|Name||Lecture Notes in Computer Science|
|Publisher||Springer International Publishing|
|Conference||Hardware and Software: Verification and Testing; 12th International Haifa Verification Conference, HVC 2016|
|Period||14/11/16 → 17/11/16|
|Other||14-17 Nov 2016|
- Model Checking
- accepting cycle
- strongly connected component