Paper Info
Title
SLMC: a tool for model checking concurrent systems against dynamical spatial logic specifications
Abstract
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.
Year
DOI
Venue
2012
10.1007/978-3-642-28756-5_35
TACAS
Keywords
Field
DocType
available tool,verifying system,concurrent system,combined analysis,spatial property,structural dynamic,spatial logic model checker,calculus system,structural property,spatial logic,dynamical spatial logic specification,open source
Model checking,Programming language,Concurrency,Computer science,Spatial logic,Software system,Theoretical computer science,Interference (wave propagation),Liveness
Conference
Volume
ISSN
Citations 
7214
0302-9743
4
PageRank 
References 
Authors
0.52
9
2
Name
Order
Citations
PageRank
Luís Caires1103763.30
Hugo Torres Vieira213411.17