VoxLogicA UI: Supporting Declarative Medical Image Analysis

Abstract

This Master's Thesis in Computer Science dives into the design and creation of a user-friendly interface for VoxLogicA, an image analysis tool using spatial model checking with a focus on neuroimaging. The research tackles the problem of existing tools being too complex, which makes them hard for medical professionals and researchers to use. By using spatial logic, the goal is to make these powerful analytical tools more practical and accessible in real-world clinical settings. The main objectives are to design a modern web interface that's easy to use, build it with the latest web technologies (e.g. Svelte and Niivue), and test its effectiveness through user studies and real-world case analyses.

Figures (13)

• Figure 1: Ariane-5 rocket's catastrophic failure during its maiden flight in 1996, costing over $370 million. The disaster was caused by a software error in the Inertial Reference System (SRI), which led to an operand error and subsequent system shutdown. Formal methods could have prevented this failure by identifying and addressing the software design flaws and exception handling issues before launch. ariane5Flight501
• Figure 2: Axial slices of a brain MRI scan from the BraTS dataset showing tumor segmentation overlaid on T1-weighted images. The segmentation shows different tumor sub-regions: the peritumoral edema (yellow/beige), the necrotic and non-enhancing tumor core (light blue), and the enhancing tumor (dark green) brats2021Kaggle.
• Figure 3: Example of brain tumor segmentation using VoxLogicA, achieving 90% Dice coefficient in 5-10 seconds for each 3D image containing 9 million data points. For more information, please check the https://vincenzoml.github.io/VoxLogicA/.
• Figure 4: Screenshot of 3D Slicer.
• Figure 5: Screenshot of VoxLogicA Explorer interface.