• Spatial Logics
• Model Checking
• GPU

Recent years witnessed the widespread use of GPUs for speeding up
computationally intensive tasks. As far as system verification is concerned, one of
such tasks is model checking, a fully automated method to check the truth value of
a logic formula at a given model. Some model checkers running entirely in GPU
have been proposed, achieving a good performance improvement with respect to
classical implementations. The thesis focus on the spatial model checker
VoxLogicA, which has been successfully used to analyse real-world datasets of MRI
scans of the human brain, identifying tumoral areas with confidence in par with
humans and best-in-class machine learning methods. We present an implementation
of VoxLogica in GPU: it exploits existing algorithms for the labelling of connected
components, which can be used to compute reachability-based spatial logic
formulas on a graph.