Luca

Computer Science researcher

University Assistant (post-doc) at TU Wien

Vienna, Vienna, Austria🇦🇹

My research mainly concerns the formal modelling and analysis of agent-based models of complex collective systems. On one hand, this entails the development of formally defined high-level languages to concisely describe the features of individual agents; on the other hand, it requires applying and improving state-of-the-art verification techniques to check the collective behaviour of the resulting system.

Keywords associated with my interests include: (Modelling): Agent-based modelling, Attribute-based communication, Collective adaptive systems, Domain-specific languages, Multi-agent systems, Process algebras, Stigmergic interaction, Structural operational semantics, Temporal logics; (Analysis): Bounded model checking, Explicit-state and symbolic model checking, Software verification, Static analysis.

Activity

Active on:Bluesky network

Loading activity...

View full activity

Career: 9

University Assistant (post-doc)

TU Wien

Full-time · On-site

Mar 2024 - Present

Model CheckingTypeScriptPythonRuntime verificationReactive SynthesisNuXmv

Postdoctoral Researcher

University of Gothenburg

Full-time · On-site

May 2022 - Feb 2024

Model CheckingReactive SynthesisNuXmvJavaPython

Supply Teacher (Vacataire d'enseignement superieur)

Université Paris-Saclay

Temporary · On-site

Mar 2022 - Apr 2022

Taught a 36-hour MSc course on "Modelling and Verification".

Model CheckingCADP

Postdoctoral Researcher

CONVECS: Construction de systèmes concurrents vérifiés

Full-time · On-site

Nov 2020 - Apr 2022

Researcher at CONVECS (Construction of Verified Concurrent Systems), a research team at INRIA Grenoble.

PythonF#CADPModel Checking

Supply Teacher (Vacataire d'enseignement superieur)

Université Paris-Saclay

Temporary · Remote

Apr 2021 - May 2021

Taught a 36-hour MSc course on "Modelling and Verification".

Grant holder (Pre-Doc)

IMT School for Advanced Studies Lucca

Fellowship · Hybrid

Dec 2019 - Nov 2020

PythonF#

Visiting PhD Student

CONVECS: Construction de systèmes concurrents vérifiés

Mar 2019 - Jul 2019

Visiting CONVECS (Construction of Verified Concurrent Systems), a research team at INRIA Grenoble.

Model CheckingPythonF#

Intern - Workshop Planning and Lines Industrialization

Thales Alenia Space (Italy)

Internship · On-site

Jun 2015 - Feb 2016

Maintenance and porting of legacy traceability systems

Microsoft SQL Server.NET

Intern

Aubay Italia

Internship

Dec 2013 - Feb 2014

BSc Thesis internship. Design and implementation of a cross-platform mobile publishing platform (Android, Windows Phone).

ASP.NET.NETMicrosoft SQL ServerAndroid DevelopmentXamarinC#

Skills: 26

Technical

.NETAndroid DevelopmentCC#C++ErlangHTML5Java

LinuxmacOSMicrosoft OfficeMicrosoft SQL ServerPHPPythonRubyTypeScript

Other

ASP.NETCADPF#Formal methodsModel CheckingNuXmvReactive SynthesisRuntime verification

Software verificationXamarin

Projects: 4

HOAX

github.com/lou1306/hoax

Aug 2024 - Present

The HOA eXecutor. A tool to run and monitor automata written in the Hanoi Omega-Automata format (HOA).

homebrew-formal

github.com/lou1306/homebrew-formal

Apr 2024 - Present

A Homebrew repository for tools related to formal methods and automated reasoning. An active fork of mht208/homebrew-formal.

R-CHECK

github.com/dsynma/rcheck

May 2022 - Present

A language and platform for modelling, simulation, and verification of reconfigurable systems. Project led by Yehia Abd Alrahman (University of Gothenburg). I am one of the main developers of the R-CHECK tooling, especially its Visual Studio Code extension.

SLiVER

github.com/labs-lang/sliver/

Nov 2017 - Present

A verifier for multi-agent systems with indirect communication mechanisms, expressed in a simple high-level formalism called LAbS.

Publications: 19

Execution and Monitoring of HOA Automata with HOAX

Book Chapter

doi.org/10.1007/978-3-032-05435-7_3

Luca Di Stefano

2026

Attributed Point-to-Point Communication in R-CHECK

Book Chapter

doi.org/10.1007/978-3-031-75107-3_20

Yehia Abd Alrahman, Shaun Azzopardi, Luca Di Stefano, Nir Piterman

2025

Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification

Book Chapter

doi.org/10.1007/978-3-031-73709-1_16

Luca Di Stefano, Omar Inverso

2025

Full LTL Synthesis over Infinite-State Arenas

Book Chapter

doi.org/10.1007/978-3-031-98685-7_13

Shaun Azzopardi, Luca Di Stefano, Nir Piterman, Gerardo Schneider

2025

Compositional verification of priority systems using sharp bisimulation

Formal Methods in System Design

Journal Article

doi.org/10.1007/s10703-023-00422-1

Luca Di Stefano, Frédéric Lang

May 2023

Compositional Verification of Stigmergic Collective Systems

Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics

Conference Paper

doi.org/10.1007/978-3-031-24950-1_8

Di Stefano, L., Lang, F.

2023

Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants

Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics

Conference Paper

doi.org/10.1007/978-3-031-42697-1_4

De Nicola, R., Di Stefano, L., Inverso, O., Valiani, S.

2023

Language support for verifying reconfigurable interacting systems

International Journal on Software Tools for Technology Transfer

Journal Article

doi.org/10.1007/s10009-023-00729-8

Alrahman, Y.A., Azzopardi, S., Di Stefano, L., Piterman, N.

2023

Modelling flocks of birds and colonies of ants from the bottom up

International Journal on Software Tools for Technology Transfer

Journal Article

doi.org/10.1007/s10009-023-00731-0

De Nicola, R., Di Stefano, L., Inverso, O., Valiani, S.

2023

Automated replication of tuple spaces via static analysis

Science of Computer Programming

Journal Article

doi.org/10.1016/j.scico.2022.102863

De Nicola, R., Di Stefano, L., Inverso, O., Uwimbabazi, A.

2022

Modelling Flocks of Birds from the Bottom Up

Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning

Book Chapter

doi.org/10.1007/978-3-031-19759-8_6

Rocco De Nicola, Luca Di Stefano, Omar Inverso, Serenella Valiani

2022

Process Algebras and Flocks of Birds

Lecture Notes in Computer Science

Book Chapter

doi.org/10.1007/978-3-031-15629-8_27

Rocco De Nicola, Luca Di Stefano, Omar Inverso, Serenella Valiani

2022

Verification of Distributed Systems via Sequential Emulation

ACM Transactions on Software Engineering and Methodology

Journal Article

doi.org/10.1145/3490387

Di Stefano, L., De Nicola, R., Inverso, O.

2022

Verifying Temporal Properties of Stigmergic Collective Systems Using CADP

Lecture Notes in Computer Science

Conference Paper

doi.org/10.1007/978-3-030-89159-6_29

Di Stefano, L., Lang, F.

2021

Combining sliver with cadp to analyze multi-agent systems

Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics

Conference Paper

doi.org/10.1007/978-3-030-50029-0_23

Di Stefano, L., Lang, F., Serwe, W.

2020

Multi-agent systems with virtual stigmergy

Science of Computer Programming

Journal Article

doi.org/10.1016/j.scico.2019.102345

De Nicola, R., Di Stefano, L., Inverso, O.

2020

Toward Formal Models and Languages for Verifiable Multi-Robot Systems

Frontiers in Robotics and AI

Journal Article

doi.org/10.3389/frobt.2018.00094

Rocco De Nicola, Luca Di Stefano, Omar Inverso

Sep 2018

Multi-agent Systems with Virtual Stigmergy

Software Technologies: Applications and Foundations

Publication

doi.org/10.1007/978-3-030-04771-9_26

Rocco De Nicola, Luca Di Stefano, Omar Inverso

2018

Reactive Obstacle Avoidance for Multicopter UAVs via Evaluation of Depth Maps

Proceedings of Workshops and Posters at the 13th International Conference on Spatial Information Theory (COSIT 2017)

Publication

doi.org/10.1007/978-3-319-63946-8_10

Luca Di Stefano, Eliseo Clementini, Enrico Stagnini

Sep 2017

Education: 3

Gran Sasso Science Institute

PhD, Computer Science

Jan 2016 - Jan 2020

Title of the Thesis: "Modelling and Verification of Multi-Agent Systems via Sequential Emulation" Supervisors: Rocco De Nicola (IMT Lucca), Omar Inverso (GSSI)