Formal methods · Artificial intelligence

Laura Bussi

Lecturer · Informatics Institute, University of Amsterdam

I am a researcher in formal methods and artificial intelligence. I work on spatial and spatio-temporal reasoning, model checking, and the verification of learning-based systems, developing logical and algorithmic foundations for trustworthy AI, with an emphasis on tool-supported methods and safety-critical applications such as medical imaging.

l.bussi@uva.nl Google Scholar GitHub CV (PDF)
Laura Bussi giving a talk
2026 · Award
Paolo Gentilini Award
For applications of logic to biomedical science — Italian Association for Logic and its Applications (AILA)
2026 · Chair
Artifact Evaluation Chair, SPIN 2026
International Symposium on Model Checking of Software
2025 · Chair
Artifact Evaluation Chair, ETAPS 2025
European Joint Conferences on Theory and Practice of Software

Research

Logical foundations for trustworthy AI

From spatial logics on images and polyhedra to verified neural networks: I build theory and tools that make it possible to reason rigorously about large, structured, and learned systems.

i.
Formal methods for reasoning about large structured systems
ii.
Spatial and topological reasoning
iii.
Neuro-symbolic artificial intelligence
iv.
Trustworthy and explainable machine learning

Publications

Selected publications

Full and up-to-date list on Google Scholar.

  1. 2026
    Spatio-temporal Model Checking with VoxLogicA
    L. Bussi, V. Ciancia, F. Gadducci, M. Massink
    Journal of Logic, Language and Information 35, 83–108 Journal
  2. 2026
    Weak Simplicial Bisimilarity and Minimisation for Polyhedral Model Checking
    N. Bezhanishvili, L. Bussi, V. Ciancia, D. Gabelaia, M. Jibladze, D. Latella, M. Massink
    Logical Methods in Computer Science 22(1) Journal
  3. 2025
    ABS: Enforcing Constraint Satisfaction on Generated Sequences via Automata-Guided Beam Search ↗
    L. Bussi, V. Collura, M. Cordy, E. Giunchiglia, K. Tit
    arXiv:2506.09701 Preprint
  4. 2024
    Logics of Polyhedral Reachability
    N. Bezhanishvili, L. Bussi, V. Ciancia, D. F. Duque, D. Gabelaia
    Advances in Modal Logic (AiML 2024) Conference
  5. 2024
    Towards Hybrid-AI in Imaging using VoxLogicA
    G. Belmonte, L. Bussi, V. Ciancia, D. Latella, M. Massink
    ISoLA 2024, LNCS 15222, 205–221 Conference
  6. 2023
    A Toolchain for Strategy Synthesis with Spatial Properties
    D. Basile, L. Bussi, V. Ciancia, M. ter Beek
    International Journal on Software Tools for Technology Transfer 25, 641–658 Journal
Other publications
  1. 2023
    A Spatial Logic with Time and Quantifiers
    L. Bussi, V. Ciancia, F. Gadducci
    DaLí: Dynamic Logic — New Trends and Applications, Springer, 1–19
  2. 2022
    On Binding in the Spatial Logic for Closure Spaces
    L. Bussi, V. Ciancia, F. Gadducci, D. Latella, M. Massink
    ISoLA 2022, Springer, 479–497
  3. 2022
    Soft Concurrent Constraint Programming with Local Variables
    L. Bussi, F. Gadducci, F. Santini
    COORDINATION 2022, Springer, 159–177
  4. 2021
    Querying Medical Imaging Datasets using Spatial Logics (position paper)
    G. Belmonte, G. Broccia, L. Bussi, V. Ciancia, D. Latella, M. Massink
    MEDI 2021, Springer, 285–301
  5. 2021
    Towards Model Checking Video Streams Using VoxLogicA on GPUs
    L. Bussi, V. Ciancia, F. Gadducci, D. Latella, M. Massink
    From Data to Models and Back (DataMod 2021), Springer, 78–90
  6. 2021
    Towards a Spatial Model Checker on GPU
    L. Bussi, V. Ciancia, F. Gadducci
    FORTE 2021, Springer, 188–196
  7. 2019
    Polyadic Soft Constraints
    L. Bussi, F. Gadducci, F. Santini
    The Art of Modelling Computational Systems, Springer, 241–257

Community

Service

Chairing & programme committees

  • 2026
    AEC Chair
    SPIN — Symposium on Model Checking of Software
  • 2025
    AEC Chair
    ETAPS — European Joint Conferences on Theory and Practice of Software
  • 2024
    PC Member, Artifact Evaluation
    FM 2024 · FoSSaCS 2024 · FormaliSE 2024
  • 2023
    PC Member, Artifact Evaluation
    FormaliSE 2023
  • 2022
    Local organiser
    ItaCa — Italian Category Theorists workshop, Pisa

Invited talks

  • Jun 2025
    Polyhedral Logic with Reachability: from Semantics to Minimization
    Topological Methods in Logic VII, Tbilisi

Reviewing

Reviewer for journals and conferences including Fuzzy Sets and Systems, the Journal of Systems and Software, NeurIPS and NeSy.

Tools

Software

Spatial model checking in practice, with a focus on medical imaging.

VoxLogicA-GPU ↗
Main developer

GPU-accelerated spatial model checker for voxel-based medical image analysis.
VoxLogicA 2 ↗
Contributor

The next generation of the VoxLogicA spatial model checker.
VoxLogicA · Kripke ↗
Contributor

Extension of VoxLogicA to Kripke structures and posets.

Teaching

Teaching

Curriculum

Short CV

Positions

  • 2025–now
    Lecturer
    Informatics Institute, University of Amsterdam
  • 2025
    Postdoctoral fellow
    SnT, University of Luxembourg — verification of neural networks
  • 2024–2025
    Postdoctoral fellow
    FMT Lab, ISTI-CNR, Pisa — AI and spatial logics for medical imaging

Research visits

  • 2025
    Imperial College London
    with Eleonora Giunchiglia
  • 2023
    Tbilisi State University
    with David Gabelaia
  • 2023
    ILLC, University of Amsterdam
    with Nick Bezhanishvili

Education

  • 2020–2024
    PhD in Computer Science, University of Pisa
    Thesis: Model checking properties with identity binding in space-time. Advisors: Fabio Gadducci, Vincenzo Ciancia
  • 2018–2020
    MSc in Computer Science, University of Pisa
    Thesis: A GPU implementation of the spatial model checker VoxLogicA
  • 2015–2018
    BSc in Computer Science, University of Pisa
    Thesis: Polyadic soft constraints
Download full CV (PDF)