Last updated: September 2025
I am a researcher at ISTI-CNR in Pisa, working in the Formal Methods & Tools Laboratory. Previously, I've been working at the IIT-CNR in Pisa, at the ILLC (University of Amsterdam), and at the Universidad Complutense in Madrid.
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 following projects:
|
EU NRPP THE: Tuscany Health Ecosystem. ECS00000017. NRPP Mission 4, Component 2 Investment 1.5. Finanziato dall'Unionne Europea - NextGenerationEU. |
|
Bilateral Agreements CNR-SRNSF (Georgia) Model Checking for Polyhedral Logics. CUP B53C23000240005 project no. #CNR-22-010. |
|
MUR PRIN STENDHAL: Spatio-Temporal Enhancement of Neural nets for
Deeply Hierarchical Automatised Logic. Finanziato dall'Unione Europea - NextGenerationEU. |
MIUR PRIN IT-MATTERS: Methods and Tools for Trustworthy Smart Systems (finished) |
My research interests include Formal Methods in Computer Science, Spatial Logics and Spatio-Temporal Model Checking, Automata and Category Theory, Artificial Intelligence, with an accent on pairing solid mathematical theories with usable tools and implementation.
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).
Selected recent work:
| Gina Belmonte, Vincenzo Ciancia, Mieke Massink: Symbolic and hybrid AI for brain tissue segmentation using spatial model checking. Artif. Intell. Medicine 167: 103154 (2025) |
| Vincenzo Ciancia, Diego Latella, Mieke Massink: Ten Years of Spatial Model Checking. Rebeca for Actor Analysis in Action 2025: 406-424 |
| Nick Bezhanishvili, Laura Bussi, Vincenzo Ciancia, David Fernández-Duque, David Gabelaia: Logics of Polyhedral Reachability. AiML 2024: 187-204 |
| Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Mamuka Jibladze, Diego Latella, Mieke Massink, Erik P. de Vink: Weak Simplicial Bisimilarity for Polyhedral Models and SLCSη. FORTE 2024: 20-38 |
| Gina Belmonte, Laura Bussi, Vincenzo Ciancia, Diego Latella, Mieke Massink: Towards Hybrid-AI in Imaging Using VoxLogicA. ISoLA (4) 2024: 205-221 |
| Davide Basile, Maurice H. ter Beek, Laura Bussi, Vincenzo Ciancia: A toolchain for strategy synthesis with spatial properties. Int. J. Softw. Tools Technol. Transf. 25(5): 641-658 (2023) |
| Laura Bussi, Vincenzo Ciancia, Fabio Gadducci: A Spatial Logic with Time and Quantifiers. DaLí 2023: 1-19 |
| Vincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink, Erik P. de Vink: Minimisation of Spatial Models Using Branching Bisimilarity. FM 2023: 263-281 |
| Vincenzo Ciancia, David Gabelaia, Diego Latella, Mieke Massink, Erik P. de Vink: On Bisimilarity for Polyhedral Models and SLCS. FORTE 2023: 132-151 |
| Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella, Mieke Massink: Geometric Model Checking of Continuous Space. Log. Methods Comput. Sci. 18(4) (2022) |
| Giovanna Broccia, Vincenzo Ciancia, Diego Latella, Mieke Massink: Towards a GUI for Declarative Medical Image Analysis: Cognitive and Memory Load Issues. HCI (38) 2022: 103-111 |
| Laura Bussi, Vincenzo Ciancia, Fabio Gadducci: Towards a Spatial Model Checker on GPU. FORTE 2021: 188-196 |
| Gina Belmonte, Giovanna Broccia, Vincenzo Ciancia, Diego Latella, Mieke Massink: Feasibility of Spatial Model Checking for Nevus Segmentation. FormaliSE@ICSE 2021: 1-12 |
| Vincenzo Ciancia, Gina Belmonte, Diego Latella, Mieke Massink: A Hands-On Introduction to Spatial Model Checking Using VoxLogicA - - Invited Contribution. SPIN 2021: 22-41 |
| Vincenzo Ciancia, Yde Venema: Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages. CALCO 2019: 5:1-5:18 |
| Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink: VoxLogicA: A Spatial Model Checker for Declarative Image Analysis. TACAS (1) 2019: 281-298 |
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.