### Abstract

Language | Undefined |
---|---|

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 |

Publisher | Springer International Publishing |

Pages | 18-33 |

Number of pages | 16 |

ISBN (Print) | 978-3-319-49051-9 |

DOIs | |

State | Published - Nov 2016 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer International Publishing |

Volume | 10028 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Keywords

- METIS-320900
- IR-102924
- Model Checking
- Multi-Core
- SCC
- accepting cycle
- LTL
- strongly connected component
- EWI-27453

### Cite this

*Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016*(pp. 18-33). (Lecture Notes in Computer Science; Vol. 10028). Cham: Springer International Publishing. DOI: 10.1007/978-3-319-49052-6_2

}

*Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016.*Lecture Notes in Computer Science, vol. 10028, Springer International Publishing, Cham, pp. 18-33. DOI: 10.1007/978-3-319-49052-6_2

**Multi-core SCC-Based LTL Model Checking.** / Bloemen, Vincent; van de Pol, Jan Cornelis.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Multi-core SCC-Based LTL Model Checking

AU - Bloemen,Vincent

AU - van de Pol,Jan Cornelis

N1 - 10.1007/978-3-319-49052-6_2

PY - 2016/11

Y1 - 2016/11

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

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

KW - METIS-320900

KW - IR-102924

KW - Model Checking

KW - Multi-Core

KW - SCC

KW - accepting cycle

KW - LTL

KW - strongly connected component

KW - EWI-27453

U2 - 10.1007/978-3-319-49052-6_2

DO - 10.1007/978-3-319-49052-6_2

M3 - Conference contribution

SN - 978-3-319-49051-9

T3 - Lecture Notes in Computer Science

SP - 18

EP - 33

BT - Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016

PB - Springer International Publishing

CY - Cham

ER -