Vincenzo Ciancia: Spatial Model Checking and Applications to Medical Image Analysis

Event Details

Spatial aspects of computation are prominent in Computer Science, especially
when dealing with systems distributed in physical space or with image data
acquired from various sources. However, formal verification techniques are
usually concerned with temporal properties and do not explicitly handle spatial

Our work stems from the topological interpretation of modal logics, the
so-called Spatial Logics. We present a topology-based approach to model checking
for spatial and spatio-temporal properties. Our results include theoretical
developments in the more general setting of Cech closure spaces, a study of a
“collective” variant, that has been compared to region calculi in recent work,
publicly available software tools, and some case studies in the setting of smart

In recent joint work with the University Hospital of Siena, we have explored the
application domain of automatic contouring in Medical Imaging, introducing the
tool VoxLogicA, which merges the state-of-the-art imaging library ITK with the
unique combination of declarative specification and optimised execution provided
by spatial model checking. The analysis of an existing benchmark of medical
images for segmentation of brain tumours shows that simple VoxLogicA
specifications can reach state-of-the-art accuracy, competing with best-in-class
algorithms based on machine learning, with the advantage of explainability and
easy replicability.


Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink:
Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science 12(4) (2016)

Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink:
VoxLogicA: A Spatial Model Checker for Declarative Image Analysis. TACAS (1) 2019: 281-298