Multi-core SCC-Based LTL Model Checking

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 3 Citations

Abstract

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.
LanguageUndefined
Title of host publicationHardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016
EditorsRoderick Bloem, Eli Arbel
Place of PublicationCham
PublisherSpringer International Publishing
Pages18-33
Number of pages16
ISBN (Print)978-3-319-49051-9
DOIs
StatePublished - Nov 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume10028
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

Bloemen, V., & van de Pol, J. C. (2016). Multi-core SCC-Based LTL Model Checking. In R. Bloem, & E. Arbel (Eds.), 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
Bloemen, Vincent ; van de Pol, Jan Cornelis. / Multi-core SCC-Based LTL Model Checking. Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016. editor / Roderick Bloem ; Eli Arbel. Cham : Springer International Publishing, 2016. pp. 18-33 (Lecture Notes in Computer Science).
@inproceedings{e3a5a85fff114958b3f21fbca474da2e,
title = "Multi-core SCC-Based LTL Model Checking",
abstract = "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.",
keywords = "METIS-320900, IR-102924, Model Checking, Multi-Core, SCC, accepting cycle, LTL, strongly connected component, EWI-27453",
author = "Vincent Bloemen and {van de Pol}, {Jan Cornelis}",
note = "10.1007/978-3-319-49052-6_2",
year = "2016",
month = "11",
doi = "10.1007/978-3-319-49052-6_2",
language = "Undefined",
isbn = "978-3-319-49051-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "18--33",
editor = "Roderick Bloem and Eli Arbel",
booktitle = "Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016",

}

Bloemen, V & van de Pol, JC 2016, Multi-core SCC-Based LTL Model Checking. in R Bloem & E Arbel (eds), 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.

Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016. ed. / Roderick Bloem; Eli Arbel. Cham : Springer International Publishing, 2016. p. 18-33 (Lecture Notes in Computer Science; Vol. 10028).

Research output: Chapter in Book/Report/Conference proceedingConference 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 -

Bloemen V, van de Pol JC. Multi-core SCC-Based LTL Model Checking. In Bloem R, Arbel E, editors, Hardware and Software: Verification and Testing; Proceedings of the 12th International Haifa Verification Conference, HVC 2016. Cham: Springer International Publishing. 2016. p. 18-33. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-49052-6_2