Multi-Core LTSmin: Marrying Modularity and Scalability

Alfons Laarman, Jan Cornelis van de Pol, M. Weber

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    34 Citations (Scopus)
    21 Downloads (Pure)

    Abstract

    The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.
    Original languageUndefined
    Title of host publicationProceedings of the Third International Symposium on NASA Formal Methods, NFM 2011
    EditorsMichaela Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi
    Place of PublicationBerlin
    PublisherSpringer
    Pages506-511
    Number of pages6
    ISBN (Print)978-3-642-20397-8
    DOIs
    Publication statusPublished - Jul 2011
    Event3rd International Symposium on NASA Formal Methods, NFM 2011 - Pasadena, United States
    Duration: 18 Apr 201120 Apr 2011
    Conference number: 3

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume6617
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference3rd International Symposium on NASA Formal Methods, NFM 2011
    Abbreviated titleNFM
    CountryUnited States
    CityPasadena
    Period18/04/1120/04/11

    Keywords

    • METIS-277604
    • IR-77023
    • tree-based algorithm
    • compression
    • EWI-20004
    • Parallel
    • Multi-Core
    • Model Checking
    • FMT-MC: MODEL CHECKING
    • incremental hashing

    Cite this

    Laarman, A., van de Pol, J. C., & Weber, M. (2011). Multi-Core LTSmin: Marrying Modularity and Scalability. In M. Bobaru, K. Havelund, G. J. Holzmann, & R. Joshi (Eds.), Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011 (pp. 506-511). (Lecture Notes in Computer Science; Vol. 6617). Berlin: Springer. https://doi.org/10.1007/978-3-642-20398-5_40
    Laarman, Alfons ; van de Pol, Jan Cornelis ; Weber, M. / Multi-Core LTSmin: Marrying Modularity and Scalability. Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. editor / Michaela Bobaru ; Klaus Havelund ; Gerard J. Holzmann ; Rajeev Joshi. Berlin : Springer, 2011. pp. 506-511 (Lecture Notes in Computer Science).
    @inproceedings{9c01a0988d65427cbfc58f9565899e70,
    title = "Multi-Core LTSmin: Marrying Modularity and Scalability",
    abstract = "The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.",
    keywords = "METIS-277604, IR-77023, tree-based algorithm, compression, EWI-20004, Parallel, Multi-Core, Model Checking, FMT-MC: MODEL CHECKING, incremental hashing",
    author = "Alfons Laarman and {van de Pol}, {Jan Cornelis} and M. Weber",
    note = "10.1007/978-3-642-20398-5_40",
    year = "2011",
    month = "7",
    doi = "10.1007/978-3-642-20398-5_40",
    language = "Undefined",
    isbn = "978-3-642-20397-8",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "506--511",
    editor = "Michaela Bobaru and Klaus Havelund and Holzmann, {Gerard J.} and Rajeev Joshi",
    booktitle = "Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011",

    }

    Laarman, A, van de Pol, JC & Weber, M 2011, Multi-Core LTSmin: Marrying Modularity and Scalability. in M Bobaru, K Havelund, GJ Holzmann & R Joshi (eds), Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. Lecture Notes in Computer Science, vol. 6617, Springer, Berlin, pp. 506-511, 3rd International Symposium on NASA Formal Methods, NFM 2011, Pasadena, United States, 18/04/11. https://doi.org/10.1007/978-3-642-20398-5_40

    Multi-Core LTSmin: Marrying Modularity and Scalability. / Laarman, Alfons; van de Pol, Jan Cornelis; Weber, M.

    Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. ed. / Michaela Bobaru; Klaus Havelund; Gerard J. Holzmann; Rajeev Joshi. Berlin : Springer, 2011. p. 506-511 (Lecture Notes in Computer Science; Vol. 6617).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Multi-Core LTSmin: Marrying Modularity and Scalability

    AU - Laarman, Alfons

    AU - van de Pol, Jan Cornelis

    AU - Weber, M.

    N1 - 10.1007/978-3-642-20398-5_40

    PY - 2011/7

    Y1 - 2011/7

    N2 - The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.

    AB - The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.

    KW - METIS-277604

    KW - IR-77023

    KW - tree-based algorithm

    KW - compression

    KW - EWI-20004

    KW - Parallel

    KW - Multi-Core

    KW - Model Checking

    KW - FMT-MC: MODEL CHECKING

    KW - incremental hashing

    U2 - 10.1007/978-3-642-20398-5_40

    DO - 10.1007/978-3-642-20398-5_40

    M3 - Conference contribution

    SN - 978-3-642-20397-8

    T3 - Lecture Notes in Computer Science

    SP - 506

    EP - 511

    BT - Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011

    A2 - Bobaru, Michaela

    A2 - Havelund, Klaus

    A2 - Holzmann, Gerard J.

    A2 - Joshi, Rajeev

    PB - Springer

    CY - Berlin

    ER -

    Laarman A, van de Pol JC, Weber M. Multi-Core LTSmin: Marrying Modularity and Scalability. In Bobaru M, Havelund K, Holzmann GJ, Joshi R, editors, Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. Berlin: Springer. 2011. p. 506-511. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-20398-5_40