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

    36 Citations (Scopus)
    22 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