Multi-core and/or symbolic model checking

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

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 languageEnglish
Title of host publication12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012
EditorsG. Luettgen, S. Merz
Place of PublicationBerlin
PublisherEASST
Number of pages7
DOIs
StatePublished - Sep 2012
Event12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012 - Bamberg, Germany

Publication series

NameElectronic Communications of the EASST
PublisherEASST
Volume53
ISSN (Print)1863-2122
ISSN (Electronic)1863-2122

Workshop

Workshop12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012
Abbreviated titleAVoCS
CountryGermany
CityBamberg
Period18/09/1220/09/12
Internet address

Fingerprint

Model checking
Specification languages

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

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). Berlin: EASST. DOI: 10.14279/tuj.eceasst.53.773

van Dijk, Tom; Laarman, Alfons; van de Pol, Jan Cornelis / Multi-core and/or symbolic model checking.

12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012. ed. / G. Luettgen; S. Merz. Berlin : EASST, 2012. 773 (Electronic Communications of the EASST; Vol. 53).

Research output: ScientificConference contribution

@inbook{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 = "9",
doi = "10.14279/tuj.eceasst.53.773",
series = "Electronic Communications of the EASST",
publisher = "EASST",
editor = "G. Luettgen and S. Merz",
booktitle = "12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012",

}

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, EASST, Berlin, 12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012, Bamberg, Germany, 18-20 September. DOI: 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 : EASST, 2012. 773 (Electronic Communications of the EASST; Vol. 53).

Research output: ScientificConference contribution

TY - CHAP

T1 - Multi-core and/or symbolic model checking

AU - van Dijk,Tom

AU - Laarman,Alfons

AU - van de Pol,Jan Cornelis

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

PB - EASST

ER -

van Dijk T, Laarman A, van de Pol JC. Multi-core and/or symbolic model checking. In Luettgen G, Merz S, editors, 12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012. Berlin: EASST. 2012. 773. (Electronic Communications of the EASST). Available from, DOI: 10.14279/tuj.eceasst.53.773