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

  • 31 Citations

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.
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 Verlag
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 Verlag. 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 Verlag, 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 Verlag",
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",
address = "Germany",

}

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 Verlag, 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 Verlag, 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 Verlag

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 Verlag. 2011. p. 506-511. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-20398-5_40