VoxLogicA: a Spatial Model Checker for Declarative Image Analysis
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.
Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 18:00 | |||
16:30 30mTalk | VoxLogicA: a Spatial Model Checker for Declarative Image Analysis TACAS Link to publication | ||
17:00 30mTalk | On Reachability in Parameterized Phaser Programs TACAS Link to publication | ||
17:30 30mTalk | Abstract Dependency Graphs and Their Application to Model CheckingBest paper nomination TACAS Link to publication |