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.
Interests. Software verification, Model checking, Multi-agent systems, Formal semantics, Process calculi
- 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
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
2020
2018
2017
Preprints and Technical Reports
2023