Vincenzo Ciancia

Vincenzo Ciancia

Senior Researcher (Primo Ricercatore), CNR-ISTI, Pisa

Formal Methods and Tools Laboratory, Institute of Information Science and Technologies “A. Faedo”, Consiglio Nazionale delle Ricerche

Spatial model checking A grid of voxels from a brain scan. A short logical specification defines core and edema; the voxels that satisfy it are coloured. let core = bright & homogeneous let edema = hyperintense & near(core) let tumour = touch(edema, core) core edema

Profile

I work on logic, formal verification and AI. My main research line is spatial model checking for image analysis, started in 2016 and developed in the VoxLogicA tools, from the underlying theory (spatial logics, bisimilarity, minimisation) to high-performance implementations and applications in medical imaging.

My current focus is AI that remains inspectable by people: hybrid AI with a strong symbolic component, and software developed by AI agents (NAIMA) under formally grounded supervision.

Open problems I’m working on

AI agents that produce new results in explainable image segmentation

Can LLM agents produce real research progress in symbolic, explainable medical image segmentation? Progress counts only if it is reproducible and the procedure stays readable by a person; a better score is not enough.

An ongoing experiment supported by the Anthropic AI for Science Program (2026), built on VoxLogicA 2.

A formally verified, high-performance spatial model checker

Can an image-analysis engine that runs unattended for weeks be both fast and correct by construction? Lazy parallel evaluation, caching and GPU kernels are where performance comes from, and also where errors hide.

VoxLogicA 2.1: the core is a formal model with automatically proved properties, and efficient implementations are derived from it.

Secure, local-first collaboration without central servers

How can people share and edit data, including research data, while keeping it encrypted and under their own control? User interface, network protocols, cryptography and performance have to be designed together, because each one constrains the others.

Nearbytes: a friend-to-friend architecture for encrypted, collaborative data spaces (JLAMP 2026).

Software developed by AI agents that can be trusted

How can software written by AI agents be trusted when no person can read all of it? Agents write code faster than it can be reviewed, so trust has to come from specifications, tests and a process that the agents cannot bypass.

NAIMA: an LLM-driven, multi-agent project-management tool that enforces software-engineering checks; it develops itself and VoxLogicA 2.1.

Selected publications

Authors in alphabetical order unless noted. Full list on DBLP.

  1. 2026Spatio-temporal Model Checking with VoxLogicA
    L. Bussi, V. Ciancia, F. Gadducci, M. Massink
    Journal of Logic, Language and Information 35(1–2):83–108
  2. 2026Weak Simplicial Bisimilarity and Minimisation for Polyhedral Model Checking
    N. Bezhanishvili, L. Bussi, V. Ciancia, D. Gabelaia, M. Jibladze, D. Latella, M. Massink, E. P. de Vink
    Logical Methods in Computer Science 22(1)
  3. 2025A Multi-Resolution Benchmark Framework for Spatial Reasoning Assessment in Neural Networks
    M. Imbriani, G. Belmonte, M. Massink, A. Tofani, V. Ciancia
    arXiv:2508.12741 (author order by contribution)
  4. 2025Symbolic and hybrid AI for brain tissue segmentation using spatial model checking
    G. Belmonte, V. Ciancia, M. Massink
    Artificial Intelligence in Medicine 167:103154
  5. 2024Towards Hybrid-AI in Imaging Using VoxLogicA
    G. Belmonte, L. Bussi, V. Ciancia, D. Latella, M. Massink
    ISoLA 2024, LNCS, pp. 205–221
  6. 2024Logics of Polyhedral Reachability
    N. Bezhanishvili, L. Bussi, V. Ciancia, D. Fernández-Duque, D. Gabelaia
    Advances in Modal Logic (AiML 2024), vol. 15, pp. 187–204
  7. 2024Weak Simplicial Bisimilarity for Polyhedral Models and SLCSηBest paper award
    N. Bezhanishvili, V. Ciancia, D. Gabelaia, M. Jibladze, D. Latella, M. Massink, E. P. de Vink
    FORTE 2024, LNCS, pp. 20–38
  8. 2023Minimisation of Spatial Models Using Branching Bisimilarity
    V. Ciancia, J. F. Groote, D. Latella, M. Massink, E. P. de Vink
    FM 2023, LNCS, pp. 263–281
  9. 2021Towards a Spatial Model Checker on GPU
    L. Bussi, V. Ciancia, F. Gadducci
    FORTE 2021, LNCS, pp. 188–196
  10. 2019VoxLogicA: A Spatial Model Checker for Declarative Image Analysis
    G. Belmonte, V. Ciancia, D. Latella, M. Massink
    TACAS 2019, LNCS, pp. 281–298

Recognition and service

Software

Projects