Multi-core and/or symbolic model checking

Tom van Dijk; Alfons Laarman; Jan Cornelis van de Pol

doi:10.14279/tuj.eceasst.53.773

Multi-core and/or symbolic model checking

Tom van Dijk, Alfons Laarman, Jan Cornelis van de Pol

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

7 Citations (Scopus)

87 Downloads (Pure)

Abstract

We review our progress in high-performance model checking. Our multi-core model checker is based on a scalable hash-table design and parallel random-walk traversal. Our symbolic model checker is based on Multiway Decision Diagrams and the saturation strategy. The LTSmin tool is based on the PINS architecture, decoupling model checking algorithms from the input specification language. Consequently, users can stay in their own specification language and postpone the choice between parallel or symbolic model checking. We support widely different specification languages including those of SPIN (Promela), mCRL2 and UPPAAL (timed automata). So far, multi-core and symbolic algorithms had very little in common, forcing the user in the end to make a wise trade-off between memory or speed. Recently, however, we designed a novel multi-core BDD package called Sylvan. This forms an excellent basis for scalable parallel symbolic model checking.

Original language	English
Title of host publication	12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012
Editors	G. Luettgen, S. Merz
Place of Publication	Berlin
Publisher	European Association for the Study of Science and Technology
Number of pages	7
DOIs	https://doi.org/10.14279/tuj.eceasst.53.773
Publication status	Published - Sept 2012
Event	12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012 - Bamberg, Germany Duration: 18 Sept 2012 → 20 Sept 2012 Conference number: 12 https://www.swt-bamberg.de/AVoCS2012/

Publication series

Name	Electronic Communications of the EASST
Publisher	EASST
Volume	53
ISSN (Print)	1863-2122
ISSN (Electronic)	1863-2122

Workshop

Workshop	12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012
Abbreviated title	AVoCS
Country/Territory	Germany
City	Bamberg
Period	18/09/12 → 20/09/12
Internet address	https://www.swt-bamberg.de/AVoCS2012/

Keywords

FMT-TOOLS
FMT-BDD: BINARY DECISION DIAGRAMS
FMT-MC: MODEL CHECKING
Symbolic model checking
hash table
IR-83425
Multi-core model checking
Scalability
parallel algorithms
Binary Decision Diagrams
METIS-293203
EWI-22550

Access to Document

10.14279/tuj.eceasst.53.773

Dijk2012Multi-coreFinal published version, 189 KB

Cite this

van Dijk, T., Laarman, A., & van de Pol, J. C. (2012). Multi-core and/or symbolic model checking. In G. Luettgen, & S. Merz (Eds.), 12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012 [773] (Electronic Communications of the EASST; Vol. 53). European Association for the Study of Science and Technology. https://doi.org/10.14279/tuj.eceasst.53.773

@inproceedings{a4c0e9567cbf407f95234bc6095d80a0,

title = "Multi-core and/or symbolic model checking",

abstract = "We review our progress in high-performance model checking. Our multi-core model checker is based on a scalable hash-table design and parallel random-walk traversal. Our symbolic model checker is based on Multiway Decision Diagrams and the saturation strategy. The LTSmin tool is based on the PINS architecture, decoupling model checking algorithms from the input specification language. Consequently, users can stay in their own specification language and postpone the choice between parallel or symbolic model checking. We support widely different specification languages including those of SPIN (Promela), mCRL2 and UPPAAL (timed automata). So far, multi-core and symbolic algorithms had very little in common, forcing the user in the end to make a wise trade-off between memory or speed. Recently, however, we designed a novel multi-core BDD package called Sylvan. This forms an excellent basis for scalable parallel symbolic model checking.",

keywords = "FMT-TOOLS, FMT-BDD: BINARY DECISION DIAGRAMS, FMT-MC: MODEL CHECKING, Symbolic model checking, hash table, IR-83425, Multi-core model checking, Scalability, parallel algorithms, Binary Decision Diagrams, METIS-293203, EWI-22550",

author = "{van Dijk}, Tom and Alfons Laarman and {van de Pol}, {Jan Cornelis}",

year = "2012",

month = sep,

doi = "10.14279/tuj.eceasst.53.773",

language = "English",

series = "Electronic Communications of the EASST",

publisher = "European Association for the Study of Science and Technology",

editor = "G. Luettgen and S. Merz",

booktitle = "12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012",

address = "Netherlands",

note = "12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012, AVoCS ; Conference date: 18-09-2012 Through 20-09-2012",

url = "https://www.swt-bamberg.de/AVoCS2012/",

}

van Dijk, T, Laarman, A & van de Pol, JC 2012, Multi-core and/or symbolic model checking. in G Luettgen & S Merz (eds), 12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012., 773, Electronic Communications of the EASST, vol. 53, European Association for the Study of Science and Technology, Berlin, 12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012, Bamberg, Germany, 18/09/12. https://doi.org/10.14279/tuj.eceasst.53.773

Multi-core and/or symbolic model checking. / van Dijk, Tom; Laarman, Alfons; van de Pol, Jan Cornelis.
12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012. ed. / G. Luettgen; S. Merz. Berlin: European Association for the Study of Science and Technology, 2012. 773 (Electronic Communications of the EASST; Vol. 53).

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

TY - GEN

T1 - Multi-core and/or symbolic model checking

AU - van Dijk, Tom

AU - Laarman, Alfons

AU - van de Pol, Jan Cornelis

N1 - Conference code: 12

PY - 2012/9

Y1 - 2012/9

N2 - We review our progress in high-performance model checking. Our multi-core model checker is based on a scalable hash-table design and parallel random-walk traversal. Our symbolic model checker is based on Multiway Decision Diagrams and the saturation strategy. The LTSmin tool is based on the PINS architecture, decoupling model checking algorithms from the input specification language. Consequently, users can stay in their own specification language and postpone the choice between parallel or symbolic model checking. We support widely different specification languages including those of SPIN (Promela), mCRL2 and UPPAAL (timed automata). So far, multi-core and symbolic algorithms had very little in common, forcing the user in the end to make a wise trade-off between memory or speed. Recently, however, we designed a novel multi-core BDD package called Sylvan. This forms an excellent basis for scalable parallel symbolic model checking.

AB - We review our progress in high-performance model checking. Our multi-core model checker is based on a scalable hash-table design and parallel random-walk traversal. Our symbolic model checker is based on Multiway Decision Diagrams and the saturation strategy. The LTSmin tool is based on the PINS architecture, decoupling model checking algorithms from the input specification language. Consequently, users can stay in their own specification language and postpone the choice between parallel or symbolic model checking. We support widely different specification languages including those of SPIN (Promela), mCRL2 and UPPAAL (timed automata). So far, multi-core and symbolic algorithms had very little in common, forcing the user in the end to make a wise trade-off between memory or speed. Recently, however, we designed a novel multi-core BDD package called Sylvan. This forms an excellent basis for scalable parallel symbolic model checking.

KW - FMT-TOOLS

KW - FMT-BDD: BINARY DECISION DIAGRAMS

KW - FMT-MC: MODEL CHECKING

KW - Symbolic model checking

KW - hash table

KW - IR-83425

KW - Multi-core model checking

KW - Scalability

KW - parallel algorithms

KW - Binary Decision Diagrams

KW - METIS-293203

KW - EWI-22550

U2 - 10.14279/tuj.eceasst.53.773

DO - 10.14279/tuj.eceasst.53.773

M3 - Conference contribution

T3 - Electronic Communications of the EASST

BT - 12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012

A2 - Luettgen, G.

A2 - Merz, S.

PB - European Association for the Study of Science and Technology

CY - Berlin

T2 - 12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012

Y2 - 18 September 2012 through 20 September 2012

ER -

Multi-core and/or symbolic model checking

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this