# Luca (@lucadistefano.eu)

Profile: https://sifa.id/p/lucadistefano.eu
Headline: Computer Science researcher
Website: https://github.com/lou1306/

## About

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.

## Experience

- **Visiting PhD Student at Inria** (2019 – 2019)
  Visiting presso il team CONVECS (Construction of Verified Concurrent Systems).
- **Intern - Workshop Planning and Lines Industrialization at Thales Alenia Space** (2015 – 2016)
  Maintenance and porting of legacy traceability systems
- **Intern at Aubay** (2013 – 2014)
  BSc Thesis internship. Design and implementation of a cross-platform mobile publishing platform (Android, Windows Phone).
- **Grant holder (Pre-Doc) at IMT School for Advanced Studies Lucca** (2019 – 2020)
- **University Assistant (post-doc) at Technische Universität Wien** (2024 – present)
- **Postdoctoral Researcher at University of Gothenburg** (2022 – 2024)
- **Supplente (Vacataire d'enseignement superieur) at Polytech Paris-Saclay** (2022 – 2022)
  "Modelling and Verification". Corso di 36 ore per studenti magistrali (filière apprentissage). Tenuto in inglese.
- **Postdoctoral Researcher at INRIA** (2020 – 2022)
  Researcher at CONVECS (Construction of Verified Concurrent Systems).
- **Supplente (Vacataire d'enseignement superieur) at Polytech Paris-Saclay** (2021 – 2021)
  "Modelling and Verification". Corso di 36 ore per studenti magistrali (filière apprentissage). Tenuto in didattica a distanza, in inglese.

## Education

- **GSSI - Gran Sasso Science Institute** — PhD, Computer Science (2016 – 2020)
- **Università degli Studi dell'Aquila** — MSc, Computer and Systems Engineering (2014 – 2016)
- **Università degli Studi dell'Aquila** — BSc, Computer and Systems Engineering (2009 – 2014)

## Skills

- Formal methods
- Python
- C#
- C
- PHP
- HTML5
- .NET
- Linux
- C++
- Java
- Erlang
- F#
- Microsoft Office
- Software verification
- Microsoft SQL Server
- ASP.NET
- Microsoft SQL Server
- Android Development
- Xamarin
- Model Checking

## Publications

- Execution and Monitoring of HOA Automata with HOAX (https://doi.org/10.1007/978-3-032-05435-7_3)
- Software artifact for "HOApp: Augmenting the Hanoi Omega-Automata Format beyond Booleans" — Zenodo
- Software artifact for "Execution and monitoring of HOA automata with HOAX" — Zenodo
- lou1306/hoax: v0.1.1 — Zenodo
- Software artifact for "Full LTL Synthesis over Infinite-state Arenas" — Zenodo
- Software artifact for "Full LTL Synthesis over Infinite-state Arenas" — Zenodo
- dSynMa/sweap-docker: v1.4 — Zenodo
- Software artifact for "Full LTL Synthesis over Infinite-state Arenas" — Zenodo
- Software artifact for "Full LTL Synthesis over Infinite-state Arenas" — Zenodo
- Software artifact for " — Zenodo
- Software artifact for " — Zenodo
- Attributed Point-to-Point Communication in R-CHECK (https://doi.org/10.1007/978-3-031-75107-3_20)
- Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification (https://doi.org/10.1007/978-3-031-73709-1_16)
- Full LTL Synthesis over Infinite-State Arenas (https://doi.org/10.1007/978-3-031-98685-7_13)
- Execution and monitoring of HOA automata with HOAX — Arxiv (http://www.scopus.com/inward/record.url?eid=2-s2.0-105012293204&partnerID=MN8TOARS)
- Video of flocking behaviour. From "Multi Agent Systems with Virtual Stigmergies" — Zenodo
- Video of flocking behaviour. From "Multi Agent Systems with Virtual Stigmergies" — Zenodo
- Synchonization in an audience of clapping agents — Zenodo
- Synchonization in an audience of clapping agents — Zenodo
- Synchonization in an audience of clapping agents — Zenodo
- Software artifact for "Full LTL Synthesis over Infinite-state Arenas" — Zenodo
- Welcome from the Chairs — Ftfjp 2024 Proceedings of the 26th ACM International Workshop on Formal Techniques for Java Like Programs Co Located with Issta 2024 (http://www.scopus.com/inward/record.url?eid=2-s2.0-85206268898&partnerID=MN8TOARS)
- Compositional verification of priority systems using sharp bisimulation — Formal Methods in System Design (http://dx.doi.org/10.1007/s10703-023-00422-1)
- Replication package for the paper: Compositional Verification of Priority Systems Using Sharp Bisimulation — Zenodo
- Replication package for the paper: Compositional Verification of Priority Systems Using Sharp Bisimulation — Zenodo
- Compositional Verification of Stigmergic Collective Systems — Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics (http://www.scopus.com/inward/record.url?eid=2-s2.0-85148695889&partnerID=MN8TOARS)
- Full LTL Synthesis over Infinite-state Arenas — Arxiv (http://www.scopus.com/inward/record.url?eid=2-s2.0-85214859716&partnerID=MN8TOARS)
- 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 (http://www.scopus.com/inward/record.url?eid=2-s2.0-85172137244&partnerID=MN8TOARS)
- Language support for verifying reconfigurable interacting systems — International Journal on Software Tools for Technology Transfer (http://www.scopus.com/inward/record.url?eid=2-s2.0-85175569715&partnerID=MN8TOARS)
- Modelling flocks of birds and colonies of ants from the bottom up — International Journal on Software Tools for Technology Transfer (http://www.scopus.com/inward/record.url?eid=2-s2.0-85172122856&partnerID=MN8TOARS)
- Replication Package for the paper: Compositional Verification of Stigmergic Collective Systems — Zenodo
- Replication Package for the paper: Compositional Verification of Stigmergic Collective Systems — Zenodo
- Automated replication of tuple spaces via static analysis — Science of Computer Programming (http://www.scopus.com/inward/record.url?eid=2-s2.0-85137266298&partnerID=MN8TOARS)
- Modelling Flocks of Birds from the Bottom Up — Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning (http://dx.doi.org/10.1007/978-3-031-19759-8_6)
- Process Algebras and Flocks of Birds — Lecture Notes in Computer Science (http://dx.doi.org/10.1007/978-3-031-15629-8_27)
- Verification of Distributed Systems via Sequential Emulation — ACM Transactions on Software Engineering and Methodology (http://www.scopus.com/inward/record.url?eid=2-s2.0-85130748937&partnerID=MN8TOARS)
- Verifying Temporal Properties of Stigmergic Collective Systems Using CADP — Lecture Notes in Computer Science (http://www.scopus.com/inward/record.url?eid=2-s2.0-85118140428&partnerID=MN8TOARS)
- 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 (http://www.scopus.com/inward/record.url?eid=2-s2.0-85087004553&partnerID=MN8TOARS)
- Multi-agent systems with virtual stigmergy — Science of Computer Programming (http://www.scopus.com/inward/record.url?eid=2-s2.0-85074721086&partnerID=MN8TOARS)
- Toward Formal Models and Languages for Verifiable Multi-Robot Systems — Frontiers in Robotics and AI
- Multi-agent Systems with Virtual Stigmergy — Software Technologies: Applications and Foundations
- Towards formal models and languages for verifiable multi-robot systems — Arxiv (http://www.scopus.com/inward/record.url?eid=2-s2.0-85169855578&partnerID=MN8TOARS)
- 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)

## Languages

- Italian (native)
- English (full_professional)
- French (limited_working)
- Swedish (elementary)
- German (elementary)

## Other profiles

- linkedin: https://www.linkedin.com/in/lou1306
- github: https://github.com/lou1306/
- website: https://lucadistefano.eu
- orcid: https://orcid.org/0000-0003-1922-3151