Marco Patrignani

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.
When there are open positions, contact me in case you are interested and you think you qualify.
Strong background in programming languages semantics is required, as well as will to move to Trento and travel internationally.

Research Group

  • Xaver Fabian, PhD student at Cispa and UniTN since September 2021
    On formal verification for Spectre V2+ variants and their secure compilation.
MSC Students & Interns
  • Riccardo Germenia, MS Intern, on UC Simulator autoextractor
  • Diego Oniarti, MS, on Iris Mechanization of ColorWasm
  • Matteo Di Noia, MS, on Mechanization of Languages for Compositional Secure Compilation
  • Alessio Faieta, MS, on GC+MS Wasm
  • Leo Jouguet, MS Intern, on Secure Composition of Spectre Countermeasures

Former Group Members and Thesis Students

Matthis Kruse, PhD candidate @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.
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), Jarkko Suominen (MSc @Unitn, 2025), Stefano Dal Mas (MSc @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)
Luca Giacometti (BSc @UniTN, 2023), Andrea Stedile (MSc @UniTN, 2023), Sacha Bordais-Poulard (MSc @UniTN, 2023), Guillaume Massal (MSc @UniTN, 2023)
Xaver Fabian (@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 (@MPI-SWS 2016-2020)
Matthias van der Hallen (@ KU Leuven, 2014)
Pieter van Geel (@ 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