Research Interests

Broadly, I am interested in formal methods, programming language and security (generally, programming language security and secure compilation).
I am an active promotor of the secure compilation research field, having developed with my collaborators:

• secure compilation criteria (modular full abstraction, trace-preserving compilation, robustly safe compilation, robust hyperproperty preservation criteria);
• proof techniques for secure compilation (trace-based backtranslation, approximate context-based backtranslation);
• instances of secure compilers in action (secure compilation for Spectre, for PMA and for high-level capability machines);
• teaching material for secure compilation (see my teaching page);
  More precisely, here is my (old/outdated) research statement.

Grants and Awards

• 2023: Prin-PNRR project: Amadeus
• 2022: Mysten Labs gift for our work on formalising Sui-Move.
• 2022: CCS Distinguished Paper Award for Automatic detection of speculative execution combinations.
• 2022: Rita Levi Montalcini grant (2022-2025).
• 2021: Novi grant for our work on robust safety for Move.
• 2019: CSF Distinguished Paper Award for Journey beyond full abstraction.

Open Positions

I do not have open positions at the moment.

Research Group

• Alessio Blascovich, PhD student co-supervised with Marco Guarnieri at IMDEA and UniTN since November 2026

MSC Students & Interns

• Riccardo Germenia, MS Intern, on UC Simulator autoextractor
• Filippo Marcon, MS, on secure compilation to ARM PAC
• Alessio Faieta, MS, on GC+MS Wasm

Former Group Members, Interns, and Thesis Students

Xaver Fabian, PhD student at Cispa and UniTN from September 2021 to October 2026 On formal verification for Spectre V2+ variants and their secure compilation.

Matthis Kruse, PhD candidate (withdrawn) @Cispa, October 2021–March 2025. On formal foundations of composition for secure compilers.

Andrea Stedile, Researcher @UniTN, February 2024–November 2025 On the Amadeus project and the Actum library. Leo Jouguet (MS Intern 2025/26).

Alessio Blascovich (MSc @Unitn 2026), Diego Oniarti (MSc @Unitn 2026)

Filippo Protto (BSc @Unitn 2026), Francesco Bogni (BSc @Unitn 2026), Andrei Riginel Ungureanu (BSc @Unitn 2026), Marco Adami (BSc @Unitn 2026), Davide Dalla Betta (BSc @Unitn 2026), Matteo Ballardin (BSc @Unitn 2026), Riccardo Finello (BSc @Unitn 2026), Goran Devetak (BSc @Unitn 2026), Matteo Lunardon (BSc @Unitn 2026), Matteo Sant’ana Casarotto (BSc @Unitn 2026), Luca Facchini (BSc @Unitn 2026), Eric Marin (BSc @Unitn 2026), Luca Tecchio (BSc @Unitn 2026), Emanuele Maccacaro (BSc @Unitn 2026),

Jarkko Suominen (MSc @Unitn, 2025), Stefano Dal Mas (MSc @Unitn, 2025),

Federico Frigerio (BSc @Unitn 2025), Filippo Lollato (BSc @Unitn 2025), Enrico Dalla Croce (BSc @Unitn 2025), Matteo Possamai (BSc @Unitn 2025), Stefano Girardi (BSc @Unitn 2025), Filippo Marcon (BSc @Unitn 2025), Michele Mattioli (BSc @Unitn 2025), Giovanni Maria Zanchetta (BSc @Unitn 2025), Andrea Carzeri (BSc @Unitn 2025), Ilya Emelyanov (BSc @Unitn 2025), Daniele Di Cesare (BSc @Unitn 2025), Giovanni Feltrin (BSc @Unitn 2025), Lorenzo Bodini (BSc @Unitn 2025), Alessio Amiri (BSc @Unitn 2025), Giulio Bazzoli (BSc @Unitn 2025), Alfredo Bombace (BSc @Unitn 2025), Luca Dematte (BSc @Unitn 2025), Lorenzo Midiri (BSc @Unitn 2025), Davide Minatel (BSc @Unitn 2025), Matteo Parma (BSc @Unitn 2025), Francesco Piazzi (BSc @Unitn 2025), Giovanni Zanibellato (BSc @Unitn 2025)

Federico Pezzato (MSc @Unitn, 2024),

Luca Podavini (BSc @Unitn, 2024), Patrick Cerka (BSc @Unitn, 2024), Matteo Possamai (BSc @Unitn, 2024), Sebastiano Tocci (BSc @Unitn, 2024), Alessio Zeni (BSc @Unitn, 2024), Luca Sartore (BSc @Unitn, 2024), Fabio Giovanazzi (BSc @Unitn, 2024), Andrea Ballarini (BSc @Unitn, 2024), Roberto Cornacchiari (BSc @Unitn, 2024), Sabin Andone (MSc @Unitn, 2024)

Andrea Stedile (MSc @UniTN, 2023), Sacha Bordais-Poulard (MSc @UniTN, 2023), Guillaume Massal (MSc @UniTN, 2023)

Luca Giacometti (BSc @UniTN, 2023)
Xaver Fabian (MSc @Cispa, 2021)
Koby Chan (@Stanford, 2020), Eric Martin (@Stanford, 2020)
Wilson Nguyen (@Stanford, 2019), Nicholas Barbier (@Stanford, 2019), Max DiGiacomo (@Stanford, 2019)
Maximilian Schwenger (@MPI-SWS, 2017)
Akram El-Korashy (MSc @MPI-SWS 2016-2020)
Matthias van der Hallen (BSc @KU Leuven, 2014)
Pieter van Geel (BSc @KU Leuven, 2013)

Professional Activity

• Keynote: @GTMFS'24 [ slides ]
• Chair: Prisc'25, Prisc'24, FCS'23, FCS'22
• Organiser/co organiser: PRISC’19, PRISC’18, 1st Secure Compilation Meeting
• PC: PLDI'26, CSF'26, POPL'26, Serim'25, Itasec'25, PLAS'24, CSF'24, Itasec'24, SecDev ‘24, Prisc'23, POPL'23, SecDev'23, Aplas'22, SecDev'22, SecDev'21, CCS'21, CSF’20, SAC’19, SAC’18, SAC’17, FCS’16, SAC’16, SAC’15, ICCSW’14
• Reviewer: JFP, CSF'21, POPL’16, CSF’15, Elsevier’s COMLAN, FOCLASA’14, GPCE’14, Scientific World Journal, IFM’13, FSEN’13, ESOP’12, IWACO’11, Dagstuhl seminar on secure compilation
• Panel member: PLMW@PLDI'21