Testing noninterference, quickly. - Catalin Hritcu; John Hughes 001; Benjamin C. Pierce; Antal Spector-Zabusky; Dimitrios Vytiniotis; Arthur Azevedo de Amorim; Leonidas Lampropoulos (ICFP, 2013)

Really Natural Linear Indexed Type Checking. - Arthur Azevedo de Amorim; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu (IFL, 2014)

A verified information-flow architecture. - Arthur Azevedo de Amorim; Nathan Collins; André DeHon; Delphine Demange; Catalin Hritcu; David Pichardie; Benjamin C. Pierce; Randy Pollack; Andrew Tolmach (POPL, 2014)

Micro-Policies: Formally Verified, Tag-Based Security Monitors. - Arthur Azevedo de Amorim; Maxime Dénès; Nick Giannarakis; Catalin Hritcu; Benjamin C. Pierce; Antal Spector-Zabusky; Andrew Tolmach (IEEE Symposium on Security and Privacy, 2015)

Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. - Yannis Juglaret; Catalin Hritcu; Arthur Azevedo de Amorim; Benjamin C. Pierce; Antal Spector-Zabusky; Andrew Tolmach (CoRR, 2015)

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. - Yannis Juglaret; Catalin Hritcu; Arthur Azevedo de Amorim; Boris Eng; Benjamin C. Pierce (CSF, 2016)

Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization. - Yannis Juglaret; Catalin Hritcu; Arthur Azevedo de Amorim; Benjamin C. Pierce (CoRR, 2016)

Binding Operators for Nominal Sets. - Arthur Azevedo de Amorim (MFPS, 2016)

Testing noninterference, quickly. - Catalin Hritcu; Leonidas Lampropoulos; Antal Spector-Zabusky; Arthur Azevedo de Amorim; Maxime Dénès; John Hughes 001; Benjamin C. Pierce; Dimitrios Vytiniotis (J. Funct. Program., 2016)

A semantic account of metric preservation. - Arthur Azevedo de Amorim; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata; Ikram Cherigui (POPL, 2017)

Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract). - Guglielmo Fachini; Catalin Hritcu; Marco Stronati; Ana Nora Evans; Théo Laurent; Arthur Azevedo de Amorim; Benjamin C. Pierce; Andrew Tolmach (CoRR, 2017)

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. - Carmine Abate; Arthur Azevedo de Amorim; Roberto Blanco; Ana Nora Evans; Guglielmo Fachini; Catalin Hritcu; Théo Laurent; Benjamin C. Pierce; Marco Stronati; Andrew Tolmach (CCS, 2018)

The Meaning of Memory Safety. - Arthur Azevedo de Amorim; Catalin Hritcu; Benjamin C. Pierce (POST, 2018)

Metric Semantics for Probabilistic Relational Reasoning. - Arthur Azevedo de Amorim; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (CoRR, 2018)

Probabilistic Relational Reasoning via Metrics. - Arthur Azevedo de Amorim; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (LICS, 2019)

Automating Compositional Analysis of Authentication Protocols. - Zichao Zhang; Arthur Azevedo de Amorim; Limin Jia 001; Corina S. Pasareanu (FMCAD, 2020)

Reconciling noninterference and gradual typing. - Arthur Azevedo de Amorim; Matt Fredrikson; Limin Jia 001 (LICS, 2020)

Learning Assumptions for Verifying Cryptographic Protocols Compositionally. - Zichao Zhang; Arthur Azevedo de Amorim; Limin Jia 001; Corina S. Pasareanu (FACS, 2021)

Netter: Probabilistic, Stateful Network Models. - Han Zhang 037; Chi Zhang; Arthur Azevedo de Amorim; Yuvraj Agarwal; Matt Fredrikson; Limin Jia 001 (VMCAI, 2021)

On Pitts' Relational Properties of Domains. - Arthur Azevedo de Amorim (CoRR, 2022)

On incorrectness logic and Kleene algebra with top and tests. - Cheng Zhang 026; Arthur Azevedo de Amorim; Marco Gaboardi (Proc. ACM Program. Lang., 2022)

Bunched Fuzz: Sensitivity for Vector Metrics. - june wunder; Arthur Azevedo de Amorim; Patrick Baillot; Marco Gaboardi (ESOP, 2023)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs. - Jérémy Thibault; Roberto Blanco; Dongjae Lee; Sven Argo; Arthur Azevedo de Amorim; Aïna Linn Georges; Catalin Hritcu; Andrew Tolmach (CCS, 2024)

Domain Reasoning in TopKAT. - Cheng Zhang 026; Arthur Azevedo de Amorim; Marco Gaboardi (ICALP, 2024)

Pipelines and Beyond: Graph Types for ADTs with Futures. - Francis Rinaldi; june wunder; Arthur Azevedo de Amorim; Stefan K. Muller (Proc. ACM Program. Lang., 2024)

Memory Safety: Uniqueness as Separation. - Pilar Selene Linares Arévalo; Arthur Azevedo de Amorim; Vincent Jackson; Liam O'Connor; Peter Schachte; Christine Rizkallah (APLAS, 2025)

Kleene Algebra with Commutativity Conditions Is Undecidable. - Arthur Azevedo de Amorim; Cheng Zhang 026; Marco Gaboardi (CSL, 2025)

Cryptis: Cryptographic Reasoning in Separation Logic. - Arthur Azevedo de Amorim; Amal Ahmed 001; Marco Gaboardi (CoRR, 2025)