Luca Di Stefano - Post-doctoral researcher at Inria

My research focuses on the specification and analysis of complex collective systems (such as multi-agent systems, robot swarms, stigmergies, and so on) and their verification via state-of-the-art verification techniques.
Interests. Software verification, Model checking, Multi-agent systems, Formal semantics, Process calculi

Curriculum Vitae

November 2020 – Now: 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 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

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]
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]

Publications

2022

Luca Di Stefano, Rocco De Nicola, Omar Inverso. Verification of Distributed Systems via Sequential Emulation, ACM Transactions on Software Engineering and Methodology, vol. 31.

2021

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

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.

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.