Publications
Check also my DBLP and Google Scholar pages.
Kleene Algebra with Commutativity Conditions Is Undecidable. With Cheng Zhang and Marco Gaboardi. CSL 2025. [ DOI | arxiv | http ]
SECOMP: Formally Secure Compilation of Compartmentalized C Programs. With Jérémy Thibault, Roberto Blanco, et al. CCS 2024. [ DOI | GitHub | arxiv | http ]
Domain Reasoning in TopKAT. With Cheng Zhang and Marco Gaboardi. ICALP 2024. [ DOI | arxiv | http ]
Pipelines and Beyond: Graph Types for ADTs with Futures. With Francis Rinaldi, june wunder, et al. POPL 2024. [ DOI | arxiv | http ]
Bunched Fuzz: Sensitivity for Vector Metrics. With june wunder, Patrick Baillot, et al. ESOP 2023. [ DOI | arxiv | http ]
On incorrectness logic and Kleene algebra with top and tests. With Cheng Zhang and Marco Gaboardi. POPL 2022. [ DOI | arxiv | http ]
Learning Assumptions for Verifying Cryptographic Protocols Compositionally. With Zichao Zhang, Limin Jia, et al. FACS 2021. [ DOI | http ]
Netter: Probabilistic, Stateful Network Models. With Han Zhang, Chi Zhang, et al. VMCAI 2021. [ DOI | .pdf ]
Automating Compositional Analysis of Authentication Protocols. With Zichao Zhang, Limin Jia, et al. FMCAD 2020. [ DOI | .pdf ]
Reconciling noninterference and gradual typing. With Matt Fredrikson and Limin Jia. LICS 2020. [ DOI | .pdf ]
Probabilistic Relational Reasoning via Metrics. With Marco Gaboardi, Justin Hsu, et al. LICS 2019. [ DOI | arxiv | http ]
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. With Carmine Abate, Roberto Blanco, et al. CCS 2018. [ DOI | arxiv | http ]
The Meaning of Memory Safety. With Cătălin Hrițcu and Benjamin C. Pierce. POST 2018. [ http ]
A methodology for micro-policies. Arthur Azevedo de Amorim. PhD thesis, University of Pennsylvania, 2017. [ .pdf ]
A semantic account of metric preservation. With Marco Gaboardi, Justin Hsu, et al. POPL 2017. [ arxiv ]
Binding Operators for Nominal Sets. Arthur Azevedo de Amorim. MFPS 2016. [ http ]
A verified information-flow architecture. With Nathan Collins, André DeHon, et al. JCS 2016. [ DOI | arxiv ]
Testing noninterference, quickly. With Cătălin Hrițcu, Leonidas Lampropoulos, et al. JFP 2016. [ DOI | arxiv ]
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. With Yannis Juglaret, Cătălin Hrițcu, et al. CSF 2016. [ DOI | arxiv ]
Micro-Policies: Formally Verified, Tag-Based Security Monitors. With Maxime Dénès, Nick Giannarakis, et al. Oakland S&P 2015. [ DOI | slides | full version ]
Really Natural Linear Indexed Type Checking. With Marco Gaboardi, Emilio Jesús Gallego Arias, et al. IFL 2014. [ DOI | arxiv ]
A verified information-flow architecture. With Nathan Collins, André DeHon, et al. POPL 2014. [ DOI | slides ]
Testing noninterference, quickly. With Cătălin Hrițcu, John Hughes, et al. ICFP 2013. [ DOI ]