Luca Di Stefano - Post-doctoral researcher

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.

NEWS From March 2024 I will join the Cyber Physical Systems research unit at TU Wien, Vienna, Austria. I am truly thankful to Nir for my stay at GU/Chalmers and wish all my colleagues at CSE enduring success in their research endeavours.

You can follow me at my new Web page. Vi ses! :)

Interests. Software verification, Model checking, Multi-agent systems, Formal semantics, Process calculi

Curriculum Vitae [pdf]

May 2022 – Present time: 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

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. My main focus is on development of the interpreter component and its integration with verification workflows (e.g., loading and replaying counterexamples). [code]
chalmers_beamer_theme - Beamer theme for Chalmers (and GU) presentations A fork of simonpf/chalmers_beamer_theme that tries to imitate the most recent presentation templates from University of Gothenburg (GU) and Chalmers. [code]

Publications

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]
Luca Di Stefano, Frédéric Lang. Compositional Verification of Priority Systems using Sharp Bisimulation, Formal Methods in System Design. [pdf]
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. [pdf]
Yehia Abd Alrahman, Shaun Azzopardi, Luca Di Stefano, Nir Piterman. Language Support for Verifying Reconfigurable Interacting Systems, Software Tools for Technology Transfer. [pdf]

2022

Rocco De Nicola, Luca Di Stefano, Omar Inverso, Aline Uwimbabazi. Automated replication of tuple spaces via static analysis, Science of Computer Programming, vol. 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, vol. 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, vol. 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, vol. 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 and Technical Reports

2023

Shaun Azzopardi, Nir Piterman, Gerardo Schneider, Luca Di Stefano. LTL Synthesis on Infinite-State Arenas defined by Programs, ArXiv. [pdf]
Luca Di Stefano, Frédéric Lang. Compositional Verification of Priority Systems using Sharp Bisimulation, INRIA Research report. [pdf]