SLMC: A tool for model checking concurrent systems against dynamical spatial logic specifications. The Spatial Logic Model Checker is a tool for verifying π-calculus systems against safety, liveness, and structural properties expressed in the spatial logic for concurrency of Caires and Cardelli. Model-checking is one of the most widely used techniques to check temporal properties of software systems. However, when the analysis focuses on properties related to resource usage, localities, interference, mobility, or topology, it is crucial to reason about spatial properties and structural dynamics. The SLMC is the only currently available tool that supports the combined analysis of behavioral and spatial properties of systems. The implementation, written in OCAML, is mature and robust, available in open source, and outperforms other tools for verifying systems modeled in π-calculus.

References in zbMATH (referenced in 74 articles , 1 standard article )

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

1 2 3 4 next

  1. Gorrieri, Roberto: A study on team bisimulation and H-team bisimulation for BPP nets (2022)
  2. Gorrieri, Roberto: Team bisimilarity, and its associated modal logic, for BPP nets (2021)
  3. Hüttel, Hans: Using session types for reasoning about boundedness in the (\pi)-calculus (2020)
  4. Fahrenberg, Uli; Křetínský, Jan; Legay, Axel; Traonouez, Louis-Marie: Compositionality for quantitative specifications (2018)
  5. Gorrieri, Roberto: Verification of finite-state machines: a distributed approach (2018)
  6. Guzman, Michell; Haar, Stefan; Perchy, Salim; Rueda, Camilo; Valencia, Frank D.: Belief, knowledge, lies and other utterances in an algebra for space and extrusion (2017)
  7. Hüttel, Hans: Using session types for reasoning about boundedness in the (\pi)-calculus (2017)
  8. Olarte, C.; Chiarugi, D.; Falaschi, M.; Hermith, D.: A proof theoretic view of spatial and temporal dependencies in biochemical systems (2016)
  9. Chiarugi, Davide; Falaschi, Moreno; Hermith, Diana; Olarte, Carlos: Verification of spatial and temporal modalities in biochemical systems (2015)
  10. Dwornikowski, Dariusz; Stroiński, Andrzej; Brzeziński, Jerzy: Towards a process calculus for REST: current state of the art (2015)
  11. Larsen, Kim G.; Mardare, Radu; Xue, Bingtian: Concurrent weighted logic (2015)
  12. Acciai, Lucia; Boreale, Michele: Deciding safety properties in infinite-state pi-calculus via behavioural types (2012)
  13. Bae, Kyungmin; Meseguer, José: A rewriting-based model checker for the linear temporal logic of rewriting (2012)
  14. Caires, Luís; Vieira, Hugo Torres: SLMC: a tool for model checking concurrent systems against dynamical spatial logic specifications (2012) ioport
  15. Flanagan, Cormac (ed.); König, Barbara (ed.): Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012. Proceedings (2012)
  16. Gadducci, Fabio; Monreale, Giacoma Valentina: A decentralised graphical implementation of mobile ambients (2011)
  17. Acciai, Lucia; Boreale, Michele: Spatial and behavioral types in the pi-calculus (2010)
  18. Acciai, Lucia; Boreale, Michele; Zavattaro, Gianluigi: On the relationship between spatial logics and behavioral simulations (2010)
  19. Gori, Roberta; Levi, Francesca: Abstract interpretation based verification of temporal properties for BioAmbients (2010)
  20. Lozes, Étienne; Villard, Jules: A spatial equational logic for the applied (\pi)-calculus (2010)

1 2 3 4 next

Further publications can be found at: