%0 Conference Proceedings %T Towards a Spatial Model Checker on GPU %+ Dipartimento di Informatica [Pisa] %+ CNR Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo” [Pisa] (CNR | ISTI) %A Bussi, Laura %A Ciancia, Vincenzo %A Gadducci, Fabio %Z Part 2: Short and Journal-First Papers %< avec comité de lecture %( Lecture Notes in Computer Science %B 41th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE) %C Valletta, Malta %Y Kirstin Peters %Y Tim A.C. Willemse %I Springer International Publishing %3 Formal Techniques for Distributed Objects, Components, and Systems %V LNCS-12719 %P 188-196 %8 2021-06-14 %D 2021 %R 10.1007/978-3-030-78089-0_12 %K Spatial logics %K Model checking %K GPU computation %Z Computer Science [cs] %Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers %X The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications. %G English %Z TC 6 %Z WG 6.1 %2 https://inria.hal.science/hal-03740266/document %2 https://inria.hal.science/hal-03740266/file/509782_1_En_12_Chapter.pdf %L hal-03740266 %U https://inria.hal.science/hal-03740266 %~ IFIP-LNCS %~ IFIP %~ IFIP-TC %~ IFIP-WG %~ IFIP-TC6 %~ IFIP-WG6-1 %~ IFIP-FORTE %~ IFIP-LNCS-12719