LTSmin is a toolset for model checking and manipulating labelled transition systems. LTSmin already connects a sizeable number of existing (verification) tools: muCRL, mcrl2, DiVinE, SPIN via an included version of SpinJa, NIPS, CADP and opaal. Moreover, it allows to reuse existing tools with new state space generation techniques. Implementing support for a new language module is in the order of 200–600 lines of C ”glue” code, and automatically yields tools for standard reachability checking (e.g., for state space generation and verification of safety properties), reachability with symbolic state storage (vector set), fully symbolic (BDD-based) reachability, distributed reachability (MPI-based), and multi-core reachability (including multi-core compression and incremental hashing). The synergy effects in the LTSmin implementation are enabled by a clean interface: all LTSmin modules work with a unifying state representation of integer vectors of fixed size, and the PINS dependency matrix which exploits the combinatorial nature of model checking problems. This splits model checking tools into three mostly independent parts: language modules, PINS optimizations, and model checking algorithms. On the other hand, the implementation of a verification algorithm based on the PINS matrix automatically has access to muCRL, mcrl2, DVE, PROMELA, opaal and ETF language modules. Finally, all tools benefit from PINS2PINS optimizations, like local transition caching (which speeds up slow state space generators), matrix regrouping (which can drastically reduce run-time and memory consumption of symbolic algorithms), partial order reduction and linear temporal logic.

References in zbMATH (referenced in 21 articles )

Showing results 1 to 20 of 21.
Sorted by year (citations)

1 2 next

  1. Rubio, Rubén; Martí-Oliet, Narciso; Pita, Isabel; Verdejo, Alberto: Metalevel transformation of strategies (2022)
  2. Rubio, Rubén; Martí-Oliet, Narciso; Pita, Isabel; Verdejo, Alberto: Strategies, model checking and branching-time properties in Maude (2021)
  3. Hajdu, Ákos; Micskei, Zoltán: Efficient strategies for CEGAR-based model checking (2020)
  4. Lijzenga, Oebele; van Dijk, Tom: Symbolic parity game solvers that yield winning strategies (2020)
  5. Finkbeiner, Bernd; Gieseking, Manuel; Hecking-Harbusch, Jesko; Olderog, Ernst-Rüdiger: Model checking data flows in concurrent network updates (2019)
  6. Garavel, Hubert: Nested-unit Petri nets (2019)
  7. van Glabbeek, Rob: Ensuring liveness properties of distributed systems: open problems (2019)
  8. Cleaveland, Rance; Roscoe, A. W.; Smolka, Scott A.: Process algebra and model checking (2018)
  9. Dalsgaard, Andreas E.; Enevoldsen, Søren; Fogh, Peter; Jensen, Lasse S.; Jepsen, Tobias S.; Kaufmann, Isabella; Larsen, Kim G.; Nielsen, Søren M.; Olesen, Mads Chr.; Pastva, Samuel; Srba, Jiří: Extended dependency graphs and efficient distributed fixed-point computation (2017)
  10. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  11. Barnat, Jiří: Quo vadis explicit-state model checking (2015)
  12. Garavel, Hubert; Lang, Frédéric; Mateescu, Radu: Compositional verification of asynchronous concurrent systems using CADP (2015)
  13. Cranen, Sjoerd; Groote, Jan Friso; Keiren, Jeroen J. A.; Stappers, Frank P. M.; de Vink, Erik P.; Wesselink, Wieger; Willemse, Tim A. C.: An overview of the mCRL2 toolset and its recent advances (2013)
  14. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  15. Barnat, Jiří; Bauch, Petr; Brim, Luboš; Češka, Milan: Designing fast LTL model checking algorithms for many-core GPUs (2012) ioport
  16. Dalsgaard, Andreas E.; Laarman, Alfons; Larsen, Kim G.; Olesen, Mads Chr.; van de Pol, Jaco: Multi-core reachability for timed automata (2012)
  17. Evangelista, Sami; Laarman, Alfons; Petrucci, Laure; van de Pol, Jaco: Improved multi-core nested depth-first search (2012)
  18. Hwong, Yi-Ling; Kusters, Vincent J. J.; Willemse, Tim A. C.: Analysing the control software of the compact Muon Solenoid experiment at the large hadron collider (2012) ioport
  19. Wijs, A. J.; Dashti, M. Torabi: Extended beam search for non-exhaustive state space analysis (2012)
  20. Laarman, Alfons; Langerak, Rom; van de Pol, Jaco; Weber, Michael; Wijs, Anton: Multi-core nested depth-first search (2011)

1 2 next

Further publications can be found at: