Arthur Azevedo de Amorim

43 papers A* 8A 3B 5Journal 24Unranked 3
YearRankTypeTitle / Venue / Authors
2026 J jnl
Cryptis: Cryptographic Reasoning in Separation Logic.
Proc. ACM Program. Lang.
Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi
2026 J jnl
Reverse Online Guessing Attacks on PAKE Protocols.
CoRR
Eloise Christian, Tejas Gadwalkar, Arthur Azevedo de Amorim, Edward V. Zieglar Jr
2025 J jnl
Cryptis: Cryptographic Reasoning in Separation Logic.
CoRR
Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi
2025 B conf
Kleene Algebra with Commutativity Conditions Is Undecidable.
CSL
Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi
2025 B conf
Memory Safety: Uniqueness as Separation.
APLAS
Pilar Selene Linares-Arévalo, Arthur Azevedo de Amorim, Vincent Jackson, Liam O'Connor, Peter Schachte, Christine Rizkallah
2024 A* conf
Domain Reasoning in TopKAT.
ICALP
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
2024 J jnl
Domain Reasoning in TopKAT.
CoRR
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
2024 J jnl
Kleene algebra with commutativity conditions is undecidable.
CoRR
Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi
2024 J jnl
Pipelines and Beyond: Graph Types for ADTs with Futures.
Proc. ACM Program. Lang.
Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, Stefan K. Muller
2024 A* conf
SECOMP: Formally Secure Compilation of Compartmentalized C Programs.
CCS
Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Catalin Hritcu, Andrew Tolmach
2024 J jnl
SECOMP: Formally Secure Compilation of Compartmentalized C Programs.
CoRR
Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Catalin Hritcu, Andrew Tolmach
2023 A conf
Bunched Fuzz: Sensitivity for Vector Metrics.
ESOP
june wunder, Arthur Azevedo de Amorim, Patrick Baillot, Marco Gaboardi
2023 J jnl
Pipelines and Beyond: Graph Types for ADTs with Futures.
CoRR
Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, Stefan K. Muller
2022 J jnl
Bunched Fuzz: Sensitivity for Vector Metrics.
CoRR
june wunder, Arthur Azevedo de Amorim, Patrick Baillot, Marco Gaboardi
2022 J jnl
On Pitts' Relational Properties of Domains.
CoRR
Arthur Azevedo de Amorim
2022 J jnl
On incorrectness logic and Kleene algebra with top and tests.
Proc. ACM Program. Lang.
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
2021 — conf
Learning Assumptions for Verifying Cryptographic Protocols Compositionally.
FACS
Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, Corina S. Pasareanu
2021 B conf
Netter: Probabilistic, Stateful Network Models.
VMCAI
Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, Limin Jia
2021 J jnl
On Incorrectness Logic and Kleene Algebra With Top and Tests.
CoRR
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi
2020 B conf
Automating Compositional Analysis of Authentication Protocols.
FMCAD
Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, Corina S. Pasareanu
2020 A* conf
Reconciling noninterference and gradual typing.
LICS
Arthur Azevedo de Amorim, Matt Fredrikson, Limin Jia
2019 A* conf
Probabilistic Relational Reasoning via Metrics.
LICS
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata
2018 J jnl
Metric Semantics for Probabilistic Relational Reasoning.
CoRR
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata
2018 — conf
The Meaning of Memory Safety.
POST
Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce
2018 A* conf
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise.
CCS
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
2018 J jnl
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise.
CoRR
Guglielmo Fachini, Catalin Hritcu, Marco Stronati, Arthur Azevedo de Amorim, Ana Nora Evans, Carmine Abate, Roberto Blanco, Théo Laurent, Benjamin C. Pierce, Andrew Tolmach
2017 J jnl
A Semantic Account of Metric Preservation.
CoRR
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui
2017 A* conf
A semantic account of metric preservation.
POPL
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui
2017 J jnl
Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract).
CoRR
Guglielmo Fachini, Catalin Hritcu, Marco Stronati, Ana Nora Evans, Théo Laurent, Arthur Azevedo de Amorim, Benjamin C. Pierce, Andrew Tolmach
2017 J jnl
The Meaning of Memory Safety.
CoRR
Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce
2016 J jnl
A verified information-flow architecture.
J. Comput. Secur.
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
2016 J jnl
Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization.
CoRR
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce
2016 A conf
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation.
CSF
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, Benjamin C. Pierce
2016 B conf
Binding Operators for Nominal Sets.
MFPS
Arthur Azevedo de Amorim
2016 J jnl
Testing noninterference, quickly.
J. Funct. Program.
Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
2015 J jnl
A Verified Information-Flow Architecture.
CoRR
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
2015 A* conf
Micro-Policies: Formally Verified, Tag-Based Security Monitors.
IEEE Symposium on Security and Privacy
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach
2015 J jnl
Really Natural Linear Indexed Type Checking.
CoRR
Arthur Azevedo de Amorim, Emilio Jesús Gallego Arias, Marco Gaboardi, Justin Hsu
2015 J jnl
Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components.
CoRR
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach
2014 A* conf
A verified information-flow architecture.
POPL
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
2014 — conf
Really Natural Linear Indexed Type Checking.
IFL
Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu
2014 J jnl
Testing Noninterference, Quickly.
CoRR
Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
2013 A conf
Testing noninterference, quickly.
ICFP
Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos