Vincenzo Ciancia


Last updated: March 2021

About Me

I am a researcher at ISTI-CNR in Pisa, working in the Formal Methods & Tools Laboratory (lab. coordinator: Maurice ter Beek). Previously, I've been working at the IIT-CNR in Pisa, at the ILLC (University of Amsterdam), and at the Universidad Complutense in Madrid.

My institutional page @ISTI-CNR

I received my Ph.D. in 2009 from the Department of Computer Science at the University of Pisa, under the supervision of Prof. Ugo Montanari. My Ph.D. thesis and subsequent work was devoted to Coalgebras, Presheaf Categories, and History Dependent Automata.

I am currently involved in the Italian MIUR PRIN project Methods and Tools for Trustworthy Smart Systems (It-Matters)

Research interests

My research interests include Formal Methods in Computer Science, Spatial Logics and Spatio-Temporal Model Checking, Automata and Category Theory, with an accent on pairing solid mathematical theories to usable, albeit prototypical tools.

Recently, my interests have been mostly focused on the VoxLogicA project, bringing formally specified expert knowledge to the realm of Medical Imaging via Model checking, in collaboration with colleagues at ISTI-CNR (Giovanna Broccia, Diego Latella, Mieke Massink), at the San Luca Hospital in Lucca (Gina Belmonte) and at the department of Computer Science in Pisa (Laura Bussi, Fabio Gadducci).

VoxLogicA website


Recent work:

Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink: Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transf. 22(2): 195-217 (2020)
Laura Bussi, Vincenzo Ciancia, Fabio Gadducci: A spatial model checker in GPU (extended version). CoRR abs/2010.07284 (2020)
Gina Belmonte, Giovanna Broccia, Vincenzo Ciancia, Diego Latella, Mieke Massink: Using Spatial Logic and Model Checking for Nevus Segmentation. CoRR abs/2012.13289 (2020, updated version to appear in the proceedings of FORMALISE 2021)
Vincenzo Ciancia, Diego Latella, Mieke Massink, Erik P. de Vink: Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations. CoRR abs/2005.05578 (2020)

Full list of published papers: @DBLP @CNR (from 2013 on)


VoxLogicA: a model checker for 2D and 3D (voxel-based) images, mostly targeted to medical imaging. In its repository, also more experimental tools are available: a variant for generic graphs, one for polyhedra (joint work with Nick Bezhanisvili, David Gabelaia, Gianluca Grilletti, Diego Latella, Mieke Massink), and a GPU-based implementation (joint work with Laura Bussi, Fabio Gadducci)

Topochecker: a topological model checker. Can verify spatio-temporal systems where space is described either by (evolving) images or by graphs.