# VoxLogicA: a Spatial Model Checker for Declarative Image Analysis (Extended Version)

arXiv: https://arxiv.org/abs/1811.05677 · HTML: https://mlsanity.com/paper/1811.05677/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Nov 2018.

## Built on by (most cited first, 4 of 4)

- [Geometric Model Checking of Continuous Space](https://mlsanity.com/paper/2105.06194/) (2021)
- [A Hybrid Deep Learning and Model-Checking Framework for Accurate Brain Tumor Detection and Validation](https://mlsanity.com/paper/2501.01991/) (2024)
- [Model Checking in Medical Imaging for Tumor Detection and Segmentation](https://mlsanity.com/paper/2501.02024/) (2025)
- [A Multi-Resolution Benchmark Framework for Spatial Reasoning Assessment in Neural Networks](https://mlsanity.com/paper/2508.12741/) (2025)

## Abstract (arXiv)

Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. We explore a new domain, namely (semi-)automatic contouring in Medical Imaging, introducing the tool VoxLogicA which merges the state-of-the-art library of computational imaging algorithms ITK with the unique combination of declarative specification and optimised execution provided by spatial logic model checking. The result is a rapid, logic based analysis development methodology. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA analysis can reach state-of-the-art accuracy, competing with best-in-class algorithms, with the advantage of explainability and replicability. Furthermore, due to a two-orders-of-magnitude speedup compared to the existing general-purpose spatio-temporal model checker topochecker, VoxLogicA enables interactive development of analysis of 3D medical images, which can greatly facilitate the work of professionals in this domain.