Luca Di Stefano

Univ.Ass. / PhD

Research Areas

Agent Based Modelling, Reactive synthesis, Formal Methods, model checking, Software Verification, Cybersecurity

About

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. I am also working on reactive synthesis and online formal techniques, such as runtime monitoring.

Thesis supervision. I am open to supervise BSc and MSc theses at TU Wien. For bureaucratic reasons, the main advisor would be professor Ezio Bartocci. Some proposals are already available on TISS (look up my last name). I am also open to discuss project proposals that overlap with my interests.

Interests. Software verification, Model checking, Multi-agent systems, Formal semantics, Process calculi, Reactive Synthesis, Static analysis

Role

PostDoc Researcher
Cyber-Physical Systems, E191-01

Contact

luca.di.stefano@tuwien.ac.at
1040 Wien, Treitlstrasse 3 / Room DE0323
vCard from TISS

Courses

Summer 2026

GPU Architectures and Computing / 182.731 VU
Scientific Research and Writing / 193.052 SE

Winter 2025

Operating Systems / 191.002 VU

Projects

RobustifAI: RobustifAI: Robustifying Generative AI through Human-Centric Integration of Neural and Symbolic Methods
2025 – 2028 / European Commission

Publications

Abd Alrahman, Y., Azzopardi, S., Di Stefano, L., Piterman, N. (2026). A compositional semantics for reconfigurable multi-mode interaction in R-CHECK. International Journal on Software Tools for Technology Transfer. Peer-reviewed.
DOI: 10.1007/s10009-026-00861-1
Di Stefano, L. (2025). Execution and Monitoring of HOA Automata with HOAX. In Runtime Verification : 25th International Conference, RV 2025, Graz, Austria, September 15–19, 2025, Proceedings (pp. 44–53). Springer, Cham. Peer-reviewed.
DOI: 10.1007/978-3-032-05435-7_3
Azzopardi, S., Di Stefano, L., Piterman, N., Schneider, G. (2025). Full LTL Synthesis over Infinite-State Arenas. In R. Piskac Z. Rakamaric (Eds.), Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part IV (pp. 274–297). Springer. Peer-reviewed.
DOI: 10.1007/978-3-031-98685-7_13
Di Stefano, L., Inverso, O. (2024). Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification. In Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola (pp. 253–270). Peer-reviewed.
DOI: 10.1007/978-3-031-73709-1_16
Abd Alrahman, Y., Azzopardi, S., Di Stefano, L., Piterman, N. (2024). Attributed Point-to-Point Communication in R-CHECK. In Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems (pp. 333–350). Springer. Peer-reviewed.
DOI: 10.1007/978-3-031-75107-3_20

Theses

Tepaev, A. (2026). Comparative evaluation of TLA+ and R-CHECK specifications [Diploma Thesis, Technische Universität Wien]. reposiTUm.
DOI: 10.34726/hss.2026.132821 / Download: PDF

And more…

Soon, this page will include additional information such as reference projects, activities as journal reviewer and editor, memberships in councils and committees, and other research activities.

Until then, please visit Luca’s research profile in TISS.