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/Facebook grant for our work on robust safety for Move.
  • 2019: CSF Distinguished Paper Award for Journey beyond full abstraction.

Open Positions

I am looking for: 
1 PhD student (at UniTN) on PL & security 
1 PhD student (at CISPA) on PL & security 
1 student researcher (at UniTN)
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.
  • Matthis Kruse, PhD student at Cispa since October 2021
    On formal foundations of composition for secure compilers.
  • Luca Giacometti, BSc student researcher at UniTN since February 2024
    On confidentiality for Move.
  • Andrea Stedile, Researcher at UniTN since February 2024

Thesis Students

  • Sabin Andone, MSc, on Exploring Rust to MSWasm Compilation
  • Matteo Zanotto, MSc, on Verification for the Sui Blockchain
  • Taras Rashkevich, MSc, on A Tagbased Filesystem in Rust
  • Alessio Zeni, BSc, on A Rust Learning Platform
  • Luca Podavini, BSc, on Move Fuzzer
  • Andrea Ballarini, BSc, on EVM to Move Compilation
  • Luca Sartore, BSc, on Jigsaw Recognition
  • Federico Frigerio, BSc, on A Rust Website for Software Faires
  • Federico Pezzato, BSc, on Rust Drivers for 3d Printers

Former Group Members and Students

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

  • Chair: Prisc'25, Prisc'24, FCS'23, FCS'22
  • Organiser/co organiser: PRISC’19, PRISC’18, 1st Secure Compilation Meeting
  • PC: CSF'24, Prisc'23, POPL'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