A Semantics for Disciplined Concurrency in COP. - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (ICTCS, 2016)

Robust Declassification by Incremental Typing. - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (Foundations of Security, Protocols, and Equational Reasoning, 2019)

A Brief Tour of Formally Secure Compilation. - Matteo Busi 001; Letterio Galletta (ITASEC, 2019)

Using Standard Typing Algorithms Incrementally. - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (NFM, 2019)

Translation Validation for Security Properties. - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (CoRR, 2019)

Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors. - Matteo Busi 001; Job Noorman; Jo Van Bulck; Letterio Galletta; Pierpaolo Degano; Jan Tobias Mühlberg; Frank Piessens (CSF, 2020)

Control-flow Flattening Preserves the Constant-Time Policy. - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (ITASEC, 2020)

Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors: Extended Version. - Matteo Busi 001; Job Noorman; Jo Van Bulck; Letterio Galletta; Pierpaolo Degano; Jan Tobias Mühlberg; Frank Piessens (CoRR, 2020)

Control-flow Flattening Preserves the Constant-Time Policy (Extended Version). - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (CoRR, 2020)

The Fox and the Hound: Comparing Fully Abstract and Robust Compilation. - Carmine Abate; Matteo Busi 001 (CoRR, 2020)

Fully Abstract and Robust Compilation: And How to Reconcile the Two, Abstractly. - Carmine Abate; Matteo Busi 001; Stelios Tsampas 001 (APLAS, 2021)

Mechanical incrementalization of typing algorithms. - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (Sci. Comput. Program., 2021)

Securing Interruptible Enclaved Execution on Small Microprocessors. - Matteo Busi 001; Job Noorman; Jo Van Bulck; Letterio Galletta; Pierpaolo Degano; Jan Tobias Mühlberg; Frank Piessens (ACM Trans. Program. Lang. Syst., 2021)

Secure Compilation All the Way Down. - Matteo Busi 001 (2021)

Towards effective preservation of robust safety properties. - Matteo Busi 001; Pierpaolo Degano; Letterio Galletta (SAC, 2022)

$ pi_{ mathbf{RA}}$: A $ pi text{-calculus}$ for Verifying Protocols that Use Remote Attestation. - Emiel Lanckriet; Matteo Busi 001; Dominique Devriese (CSF, 2023)

A Recipe for Cost-Effective Secure IoT: the Safe Place Project Case Study. - Francesco Palmarini; Leonardo Veronese; Matteo Busi 001; Riccardo Focardi; Flaminia L. Luccio (CSR, 2023)

Bridging the Gap: Automated Analysis of Sancus. - Matteo Busi 001; Riccardo Focardi; Flaminia L. Luccio (CSF, 2024)

Strands Rocq: Why is a Security Protocol Correct, Mechanically? - Matteo Busi 001; Riccardo Focardi; Flaminia L. Luccio (CSF, 2025)

Work-in-Progress: Optimizing Performance of User Revocation in Cryptographic Access Control with Trusted Execution Environments. - Ion Andy Ditu; Stefano Berlato; Matteo Busi 001; Roberto Carbone; Silvio Ranise (EuroS&P (Workshops), 2025)

Automated Analysis of Key Management Policies. - Matteo Busi 001; Riccardo Focardi; Sana Gul; Flaminia L. Luccio (ITASEC/SERICS, 2025)