Luca Di Stefano - University assistant (Post-doc)

My research focuses on the specification of complex collective systems (such as multi-agent systems, robot swarms, stigmergies, and so on) and their analysis via state-of-the-art verification techniques. I am also working on reactive synthesis and online formal techniques, such as runtime monitoring.
Thesis supervision. I am open to supervise BSc and MSc theses at TU Wien. For bureaucratic reasons, the main advisor would be professor Ezio Bartocci. Some proposals are already available on TISS (look up my last name). I am also open to discuss project proposals that overlap with my interests.
Interests. Software verification, Model checking, Multi-agent systems, Formal semantics, Process calculi, Reactive Synthesis, Static analysis

Latest News [archive]

2026-05-11: I have joined the FMCAD'26 Program Committee. [Read more]
2026-04-18: Our paper “Sweap: Reactive Synthesis for Infinite-State Integer Problems” has been accepted to CAV 2026. [Read more]
2026-02-18: Our paper “A Compositional Semantics for Reconfigurable Multi-Mode Interaction in R-CHECK” has been accepted for publication in the International Journal of Software Tools for Technology Transfer (STTT). [Read more]
2026-01-30: I have joined the ASQAP 2026 program committee. [Read more]
2025-09-25: I have joined the VMCAI'26 artifact evaluation committee. [Read more]

Curriculum Vitae [pdf]

March 2024 – Present time: University assistant at the CPS research unit (TU Wien, Vienna, Austria).
May 2022 – February 2024: Post-doctoral researcher at the d-SynMA team (University of Gothenburg and Chalmers, Gothenburg, Sweden).
November 2020 – April 2022: Post-doctoral researcher at CONVECS (INRIA and LIG, Grenoble, France).
December 2019 – October 2020: Holder of a research grant on “Verification of Emerging Properties in Collective Adaptive Systems” at SysMA (IMT School for Advanced Studies, Lucca, Italy).
March 2019 – July 2019: Visiting PhD student at CONVECS (INRIA and LIG, Grenoble, France).
October 2016 – November 2020: PhD in Computer Science at Gran Sasso Science Institute (L’Aquila, Italy).
March 2014 – October 2016: Master’s Degree in Computer and Systems Engineering at DISIM (University of L’Aquila, Italy).

Teaching

October 2025 – February 2026: Operating Systems, TU Wien (course Web page). Teaching assistant; course held by professor Peter Puschner. I am responsible for the planning of lab activities and practical exams, and hold part of the practical classes (Übungen) on UNIX, Linux, and systems programming in C.
2025 – 2026: Scientific Research and Writing, TU Wien. Introduction to science and the operation of the scientific community; based on a self-chosen or a given topic, students practice developing a research question, performing a literature search, basic skills of scientific writing, and giving a scientific presentation. I held a series of seminars on how to read and referee scientific papers, and how survey the scientific literature on a given topic.
2024 – 2026: “GPU Architectures and Computing”, TU Wien (course Web page). Teaching assistant; course held by professor Ezio Bartocci. The course aims ad understanding GPU computer architectures, becoming familiar with GPU programming models and environments, and solving problems through GPU programming (CUDA). I assisted in supervision and grading of group assignments related to the course.
Spring 2023 – Fall 2023:
“Principles of Concurrent Programming”, University of Gothenburg and Chalmers. Teaching assistant; course held by Gerardo Schneider (spring 2023) and Nir Piterman (fall 2023). My duties included assisting students during lab hours, grading assignments and exams, an holding part of a tutorial on Erlang.
From the syllabus of the course: This course aims to provide an introduction to the principles underlying concurrent systems, as well as to practical programming solutions for modeling and exploiting concurrency in programs. Domains where such principles and practices are relevant include operating systems, distributed systems, real-time systems, and multicore architectures.
2021 – 2022:
“Modelling and Verification”, Polytech Paris-Saclay. 36-hour course for Master students in Computer Science Engineering (filière apprentissage), which I held as a supply teacher (intervenant vacataire). The course was held remotely in 2021 and on-site in 2022. Topics included:
- Communicating automata, behavioural equivalences;
- Timed automata;
- Process algebras, temporal logics, model checking;
- Model-based testing;
- Lab sessions involving UPPAAL, CADP, TESTOR.

Software Projects

LAbS - A Language with Attribute-Based Stigmergies LAbS is a small language for multi-agent systems with stigmergic interaction. “Stigmergy” is a mechanism by which agents influence other agents' behavior by leaving traces on a shared medium. This is commonplace in biology. In LAbS, the medium is a distributed key-value store that also supports attribute-based constraints on participants. Thus, specific conditions for interaction between agents can be expressed in the form of predicates over their exposed features. This combination allows to naturally model a wide selection of systems. [code]
SLiVER - A verification tool for LAbS systems SLiVER is a tool to analyse multi-agent systems specified in the LAbS language. Currently, it support under-approximated analysis via bounded model checking, or analisys of the full state space via explicit-state model checking. Moreover, the C programs generated from SLiVER can be analyzed with several other techniques. [code]
R-CHECK - Model checking of reconfigurable multi-agent systems The R-CHECK tool includes a language to specify reconfigurable multi-agent systems, and supports model checking of thesespecifications through the state-of-the-art model checker nuXmv. R-CHECK is being developed as part of the D-SynMA project led by Nir Piterman, and the SynTM research grant held by Yehia Abd Alrahman. My main focus is on development of the interpreter component and on integration with Visual Studio Code. [code]
sweap - A symbolic approach to reactive synthesis sweap is a prototype tool that implements a symbolic approach to reactive synthesis. The setting is that of an arena defined as a symbolic automaton, possibly infinite-state, and an LTL objective (modulo theories: we currently support Linear Integer Arithmetics). The output is a controller or counterstrategy in HOA format. I collaborate with lead developer Shaun Azzopardi in the implementation of the tool. [code]
pyXmv - (Unofficial) Python interface to nuXmv pyxmv is a (very much WIP) Python wrapper for the nuXmv model checker. It aims at providing APIs for several features (LTL model checking, simulation, etc.), and comes with a small command-line tool to showcase its capabilities. [code]
hoax - Execution and monitoring of HOA automata HOAX (HOA eXecutor) executes one or more automata expressed in HOA format. Execution may be customised in several ways by means of configuration files. [code]

Publications

2026

Yehia Abd Alrahman, Shaun Azzopardi, Luca Di Stefano, Nir Piterman. A Compositional Semantics for Reconfigurable Multi-Mode Interaction in R-CHECK, Software Tools for Technology Transfer. [pdf] [code]
Shaun Azzopardi, Luca Di Stefano, Nir Piterman. sweap: Reactive Synthesis for Infinite-State Integer Problems, CAV 2026 (to appear). [pdf] [artifact] [code]

2025

Luca Di Stefano. Execution and monitoring of HOA automata with HOAX, RV 2025. [pdf] [artifact] [code] [slides]
Shaun Azzopardi, Luca Di Stefano, Nir Piterman, Gerardo Schneider. Full LTL Synthesis over Infinite-state Arenas, CAV 2025. [pdf] [artifact] [code]

2024

Luca Di Stefano, Frédéric Lang. Compositional Verification of Priority Systems using Sharp Bisimulation, Formal Methods in System Design 62. [pdf]
Luca Di Stefano, Omar Inverso. Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification, ISoLA 2024. [pdf] [code] [slides]
Yehia Abd Alrahman, Shaun Azzopardi, Luca Di Stefano, Nir Piterman. Attributed Point-to-Point Communication in R-CHECK, ISoLA 2024. [pdf] [code]

2023

Rocco De Nicola, Luca Di Stefano, Omar Inverso, Serenella Valiani. Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants, CMSB 2023. [pdf] [slides]
Luca Di Stefano, Frédéric Lang. Compositional verification of stigmergic collective systems, VMCAI 2023. [pdf] [slides]
Rocco De Nicola, Luca Di Stefano, Omar Inverso, Serenella Valiani. Modelling Flocks of Birds and Colonies of Ants from the Bottom Up, Software Tools for Technology Transfer 25. [pdf]
Yehia Abd Alrahman, Shaun Azzopardi, Luca Di Stefano, Nir Piterman. Language Support for Verifying Reconfigurable Interacting Systems, Software Tools for Technology Transfer 25. [pdf]

2022

Rocco De Nicola, Luca Di Stefano, Omar Inverso, Aline Uwimbabazi. Automated replication of tuple spaces via static analysis, Science of Computer Programming 223. [pdf]
Rocco De Nicola, Luca Di Stefano, Omar Inverso, Serenella Valiani. Process Algebras and Flocks of Birds, A journey from process algebra via timed automata to model learning - Essays dedicated to Frits Vaandrager on the occasion of his 60th birthday. [pdf]
Rocco De Nicola, Luca Di Stefano, Omar Inverso, Serenella Valiani. Modelling Flocks of Birds from the Bottom Up, ISoLA 2022. [pdf]
Luca Di Stefano, Rocco De Nicola, Omar Inverso. Verification of Distributed Systems via Sequential Emulation, ACM Transactions on Software Engineering and Methodology 31. [pdf]

2021

Luca Di Stefano, Frédéric Lang. Verifying temporal properties of stigmergic collective systems using CADP, ISoLA 2021. [pdf] [slides]

2020

Luca Di Stefano, advisors: Rocco De Nicola and Omar Inverso. Modelling and Verification of Multi-Agent Systems via Sequential Emulation, PhD thesis. [pdf]
Luca Di Stefano, Frédéric Lang, Wendelin Serwe. Combining SLiVER with CADP to Analyze Multi-agent Systems, COORDINATION 2020. [pdf] [slides] [video]
Rocco De Nicola, Luca Di Stefano, Omar Inverso. Multi-agent systems with virtual stigmergy, Science of Computer Programming 187. [pdf]

2018

Rocco De Nicola, Luca Di Stefano, Omar Inverso. Toward Formal Models and Languages for Verifiable Multi-Robot Systems, Frontiers in Robotics and AI 5.

2017

Luca Di Stefano, Eliseo Clementini, Enrico Stagnini. Reactive Obstacle Avoidance for Multicopter UAVs via Evaluation of Depth Maps, COSIT Workshops and Posters 2017.

Preprints, Technical Reports, Presentations, Supervised Theses

2025

Luca Di Stefano (joint work with S. Azzopardi, N. Piterman, G. Schneider). Reactive synthesis of LTL objectives on infinite arenas, Presentation (from CAV'25) at the VASSAL Workshop 2025. Graz, Austria. [slides]
Benjamin Stolz. Type checking a novel language for reconfigurable multi-agent systems, Bachelor’s thesis. TU Wien, Austria. [pdf]

2024

Luca Di Stefano. Software verification: from programs to complex systems, Invited seminar. University of Parma, Italy. [slides]

2023

Love Lyckaro. Evaluating in-memory caching strategies for distributed Web services, Master’s thesis. Chalmers University of Technology and University of Gothenburg, Sweden. [pdf]
Shaun Azzopardi, Nir Piterman, Gerardo Schneider, Luca Di Stefano. LTL Synthesis on Infinite-State Arenas defined by Programs, ArXiv. [pdf]

2022

Luca Di Stefano, Frédéric Lang. Compositional Verification of Priority Systems using Sharp Bisimulation, INRIA Research report. [pdf]

2019

Rocco De Nicola, Luca Di Stefano, Omar Inverso. Multi-Agent (Smart) Systems with Virtual Stigmergies, IT-MATTERS project kickoff meeting. Pisa, Italy. [slides]