Arthur Azevedo de Amorim

According to our database, Arthur Azevedo de Amorim authored at least 29 papers between 2013 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

Reverse Online Guessing Attacks on PAKE Protocols.

Eloise Christian, Tejas Gadwalkar, Arthur Azevedo de Amorim, Edward V. Zieglar Jr

CoRR, February, 2026

Cryptis: Cryptographic Reasoning in Separation Logic.

Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi

Proc. ACM Program. Lang., 2026

2025

Kleene Algebra with Commutativity Conditions Is Undecidable.

Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi

Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic, 2025

Memory Safety: Uniqueness as Separation.

Pilar Selene Linares-Arévalo, Arthur Azevedo de Amorim, Vincent Jackson, Liam O'Connor, Peter Schachte, Christine Rizkallah

Proceedings of the Programming Languages and Systems - 23rd Asian Symposium, 2025

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., January, 2024

Domain Reasoning in TopKAT.

Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi

Proceedings of the 51st International Colloquium on Automata, Languages, and Programming, 2024

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

Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024

2023

Bunched Fuzz: Sensitivity for Vector Metrics.

june wunder, Arthur Azevedo de Amorim, Patrick Baillot, Marco Gaboardi

Proceedings of the Programming Languages and Systems, 2023

2022

On incorrectness logic and Kleene algebra with top and tests.

Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi

Proc. ACM Program. Lang., 2022

On Pitts' Relational Properties of Domains.

Arthur Azevedo de Amorim

CoRR, 2022

2021

Netter: Probabilistic, Stateful Network Models.

Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, Limin Jia

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Learning Assumptions for Verifying Cryptographic Protocols Compositionally.

Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, Corina S. Pasareanu

Proceedings of the Formal Aspects of Component Software - 17th International Conference, 2021

2020

Reconciling noninterference and gradual typing.

Arthur Azevedo de Amorim, Matt Fredrikson, Limin Jia

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Automating Compositional Analysis of Authentication Protocols.

Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, Corina S. Pasareanu

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019

Probabilistic Relational Reasoning via Metrics.

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

2018

Metric Semantics for Probabilistic Relational Reasoning.

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata

CoRR, 2018

The Meaning of Memory Safety.

Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce

Proceedings of the Principles of Security and Trust - 7th International Conference, 2018

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

Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

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

A semantic account of metric preservation.

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

Testing noninterference, quickly.

Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis

J. Funct. Program., 2016

Binding Operators for Nominal Sets.

Arthur Azevedo de Amorim

Proceedings of the Thirty-second Conference on the Mathematical Foundations of Programming Semantics, 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

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation.

Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, Benjamin C. Pierce

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

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

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

Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

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

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Really Natural Linear Indexed Type Checking.

Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu

Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, 2014

2013

Testing noninterference, quickly.

Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013