Multi-core and/or symbolic model checking

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

    7 Citations (Scopus)
    44 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 languageEnglish
    Title of host publication12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012
    EditorsG. Luettgen, S. Merz
    Place of PublicationBerlin
    PublisherEuropean Association for the Study of Science and Technology
    Number of pages7
    DOIs
    Publication statusPublished - Sep 2012
    Event12th International Workshop on Automated Verification of Critical Systems, AVoCS 2012 - Bamberg, Germany
    Duration: 18 Sep 201220 Sep 2012
    Conference number: 12
    https://www.swt-bamberg.de/AVoCS2012/

    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

    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

    Fingerprint Dive into the research topics of 'Multi-core and/or symbolic model checking'. Together they form a unique fingerprint.

  • 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: European Association for the Study of Science and Technology. https://doi.org/10.14279/tuj.eceasst.53.773