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.
  • Andrea Stedile, Researcher at UniTN since February 2024
    On the Amadeus project and the Actum library.
MSc, BSc Thesis Students & Interns
  • Stefano Dal Mas, MS Intern, on ColorWasm Formalisation
  • Riccardo Germenia, MS Intern, on UC Simulator autoextractor
  • Taras Rashkevich, MSc, on A Tagbased Filesystem in Rust
  • Lorenzo Bodini, BSc, on 2d Trentino Trasporti Visualizer
  • Lorenzo Cattai, BSc, on Rust Godot
  • Ilya Emeliyanov, BSc, on Hackaprompt VisualCode plugin
  • Federico Frigerio, BSc, on A Rust Website for Software Faires
  • Marcel Stolin, BSc, on ETAS-related thesis
  • Giovanni Feltrin, BSc
  • Matteo Possamai, BSc, Raytracing in Rust
  • Enrico Dalla Croce, BSc, Raytracing in Rust
  • Michele Mattioli, BSc, Ipergrafi in Rust
  • Jarkko Suominen, MSc
  • Artem Buev, BSc
  • Giovanni Maria Zanchetta, BSc
  • Stefano Girardi, BSc

Former Group Members and Students

Matthis Kruse, PhD candidate @Cispa, October 2021–March 2025. On formal foundations of composition for secure compilers. 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: 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