How can domain experts in (medical) image analysis formalise, execute, improve, and share their methods -- for instance, to identify brain tumours in 3D Magneto-Resonance scans -- with solid guarantees that their findings are portable, predictable and reproducible, and with minimal requirements on their skills and expertise in computing?
VoxLogicA is an instrument designed to support image analysis with an emphasis on simplicity, focused on producing explainable and implementation-independent results. A VoxLogicA session is a textual specification of analysis, employing a combination of spatial features (distance between regions, or inter-reachability), with texture similarity, statistical, and imaging primitives.
VoxLogicA sessions are written using a declarative logical language, named ImgQL ("Image Query Language"), inspired by widely recognised appliances such as the "Structured Query Language" (SQL) for databases, with strong mathematical foundations rooted in the area of Spatial Logics for Topological Spaces.
VoxLogicA is a publicly distributed, free and open source software. At its heart lays a "model checker", that is, a very efficient computation engine for logical queries, exploiting advanced techniques such as memoization, and multithreading, to deliver top-notch performance.
In recent research, part of a collaboration between the "Formal Methods and Tools" group of ISTI-CNR, and Azienda Ospedaliera Universitaria Senese, VoxLogicA was used to produce a specification of just ten lines of text, that can identify Glioblastoma in a 3D Magneto-Resonance scan in 8 seconds, on a standard laptop. For comparison, the time it takes for an expert radiotherapist to perform this task is about half an hour.
The same procedure has been applied to circa 200 cases (the well-known "BRAin Tumour Segmentation (BRATS) challenge" dataset). Accuracy of the obtained results can be measured; the new procedure scores among the top ranking methods of the BRATS challenge in 2017 -- the state of the art in the field, dominated by machine-learning methods -- and it is comparable to manual delineation by human experts.
Indeed, it will be very relevant in the near future to enhance this work, both in the direction of clinical case studies, and to embrace other computational approaches, that can be coordinated and harmonised using high-level logical specifications.
A forthcoming publication introducing the tool and its applications to glioblastoma segmentation will be presented at the "25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)", affiliated to "European Joint Conferences on Theory and Practice of Software (ETAPS)":
G. Belmonte, V. Ciancia, D. Latella, M. Massink. "VoxLogicA: a Spatial Model Checker for Declarative Image Analysis".
The source code and binaries of VoxLogicA are available at:
https://github.com/vincenzoml/VoxLogicA
together with a simple example of a 2D background removal task, meant to be a tutorial for the tool
Focus