Model-Checking Spatial Properties of Concurrent Systems

In addition to behavioral properties, spatial logics can talk about other key properties of concurrent systems such as secrecy, freshness, usage of resources, and distribution. We present, in a quite informal and tutorial style, a spatial logic for systems modeled in the pi-calculus, and discuss the implementation of a model-checking tool. [Work funded by the FET IST Project Profundis].