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, Static analysis

News [archive]

2024-11-07: On Dec 9, 2024 I will be giving an invited seminar at University of Parma, Italy. [Read more]
2024-09-26: I have joined the ASQAP 2025 program committee. [Read more]
2024-08-06: Omar Inverso confirmed as keynote speaker at FTfJP'24. [Read more]
2024-07-22: I have joined the NSAD 2024 program committee. [Read more]
2024-07-03: Papers “Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification” and “Attributed Point-to-point Communication in R-Check” accepted to ISoLA'24. [Read more]
2024-06-17: Deadline extension for FTfJP'24. [Read more]
2024-04-15: I will chair the FTfJP'24 workshop at ECOOP'24. [Read more]
2024-02-16: From March 2024 I will join the Cyber Physical Systems research unit at TU Wien, Vienna, Austria. [Read more]
2024-01-23: I have joined the FMICS'24 Program Committee.

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

April 2024 – July 2024: “GPU Architectures and Computing”, TU Wien (course Web page). Teaching assistant (approx. 30 hours). The course aimed 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.
August 2023 – October 2023: “Principles of Concurrent Programming”, University of Gothenburg and Chalmers. Acted as one of the teaching assistants to course professor Nir Piterman. See below for further information about the course.
January 2023 – March 2023:
“Principles of Concurrent Programming”, University of Gothenburg and Chalmers. Acted as one of the teaching assistants to course professor Gerardo Schneider. 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.
March 2022 – April 2022: “Modelling and Verification”, Polytech Paris-Saclay. 36-hour course for Master students in Computer Science Engineering (filière apprentissage). Held as a supply teacher (intervenant vacataire). See below for further information about the course.
April 2021 – May 2021:
“Modelling and Verification”, Polytech Paris-Saclay. 36-hour course for Master students in Computer Science Engineering (filière apprentissage). Held remotely as a supply teacher (intervenant vacataire). Topics:
- Communicating automata, behavioural equivalences;
- Timed automata;
- Process algebras, temporal logics, model checking;
- Model-based testing;
- Lab sessions involving UPPAAL, CADP, TESTOR.

Projects

LAbS - A Language with Attribute-Based Stigmergies LAbS is a small language for multi-agent systems with stigmergic interaction. The term “stigmergy” denotes a mechanism that allows agents to influence each other’s behavior by leaving traces in a shared medium. In LAbS, such medium is provided by a distributed data structure that also supports attribute-based constraints. 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 for the analysis of multi-agent systems specified in the LAbS language. Currently, it support under-approximate 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 its integration with verification workflows (e.g., loading and replaying counterexamples). [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 (modulo theories) objective. The output is a controller or counterstrategy in HOA format. Currently the only theory implemented is that of Linear Integer Arithmetic. I collaborated 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]

Publications

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] [slides]
Yehia Abd Alrahman, Shaun Azzopardi, Luca Di Stefano, Nir Piterman. Attributed Point-to-Point Communication in R-CHECK, ISoLA 2024. [pdf]

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, Invited Presentations

2024

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

2023

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]