ETD system

Electronic theses and dissertations repository

 

Tesi etd-07032020-111024


Thesis type
Tesi di laurea magistrale
Author
BUSSI, LAURA
URN
etd-07032020-111024
Title
A GPU based implementation of the spatial model checker VoxLogicA
Struttura
INFORMATICA
Corso di studi
INFORMATICA
Supervisors
relatore Prof. Gadducci, Fabio
relatore Prof. Ciancia, Vincenzo
Parole chiave
  • Spatial Logics
  • Model Checking
  • GPU
Data inizio appello
09/10/2020;
Consultabilità
Completa
Riassunto analitico
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.
File