I am an assistant professor in the Department of Computer Science at the Rochester Institute of Technology. I work on making software more secure and reliable using techniques based on formal verification, programming languages and type systems.

Short bio: I pursued my Ph.D. studies at the University of Pennsylvania, under the supervision of Benjamin Pierce and co-advised by Cătălin Hrițcu. After my Ph.D., I held postdoctoral appointments at Boston University and atCarnegie Mellon. As an undergraduate student, I majored in computer science and engineering at Unicamp and Polytechnique. I am one of the authors of Software Foundations, an introductory textbook to the Coq proof assistant, and write about Coq in my blog.

E-mail: arthur.aa@gmail.com

Office: GOL-3547

News

January 2024 Our draft SECOMP: Formally Secure Compilation of Compartmentalized C Programs is out.

Our paper Pipelines and Beyond: Graph Types for ADTs with Futures appeared at POPL 2024 (available here).

January 2023 I have started as assistant professor at RIT.

February 2022 I am serving on the program committee of MFPS 2022.

November 2021 I am serving on the program committee of ICFP 2022. I am also serving as one of the ICFP Workshop co-chairs, along with Zoe Paraskevopoulou.

I am serving on the program committee of WoLLIC 2022.

September 2021 Our paper On Incorrectness Logic and Kleene Algebra with Top and Tests was selected to appear at POPL 2022 (arxiv).

July 2021 Our draft Cryptis: Composition and Separation in Cryptographic Protocols is out.

I am serving on the program committee of PriSC 2022.

November 2020 Our paper Netter: Probabilistic, Stateful Network Models was accepted at VMCAI 2021.

I am serving on the CoqPL 2021 program committee.

July 2020 Our short paper Automating Compositional Analysis of Authentication Protocols was accepted at FMCAD 2020.

April 2020 Our paper Reconciling Noninterference and Gradual Typing was accepted at LICS 2020.

March 2020 I am serving on the artifact evaluation committee for PLDI 2020.

Teaching

Spring 2024: CSCI 344 01 (RIT): Programming Language Concepts

Fall 2023: CSCI 740 (RIT): Programming Language Theory

Spring 2023: CSCI 344 01 (RIT): Programming Language Concepts

Spring 2022: CS 599 G1 (BU): Formal Proofs about Programs

Publications

Check also my DBLP and Google Scholar pages.

Pipelines and Beyond: Graph Types for ADTs with Futures. Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, and Stefan K. Muller. Proc. ACM Program. Lang., 8(POPL):482--511, 2024. [ DOI | arxiv | http ]

Bunched Fuzz: Sensitivity for Vector Metrics. june wunder, Arthur Azevedo de Amorim, Patrick Baillot, and Marco Gaboardi. In Thomas Wies, editor, Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13990 of Lecture Notes in Computer Science, pages 451--478. Springer, 2023. [ DOI | arxiv | http ]

On incorrectness logic and Kleene algebra with top and tests. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Proc. ACM Program. Lang., 6(POPL):1--30, 2022. [ DOI | arxiv | http ]

Learning Assumptions for Verifying Cryptographic Protocols Compositionally. Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina S. Pasareanu. In Gwen Salaün and Anton Wijs, editors, Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, October 28-29, 2021, Proceedings, volume 13077 of Lecture Notes in Computer Science, pages 3--23. Springer, 2021. [ DOI | http ]

Netter: Probabilistic, Stateful Network Models. Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, and Limin Jia. In Fritz Henglein, Sharon Shoham, and Yakir Vizel, editors, Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, pages 486--508. Springer, 2021. [ DOI | .pdf ]

Automating Compositional Analysis of Authentication Protocols. Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina S. Pasareanu. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 113--118. IEEE, 2020. [ DOI | .pdf ]

Reconciling noninterference and gradual typing. Arthur Azevedo de Amorim, Matt Fredrikson, and Limin Jia. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 116--129. ACM, 2020. [ DOI | .pdf ]

Probabilistic Relational Reasoning via Metrics. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1--19, 2019. [ DOI | arxiv | http ]

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hrițcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 1351--1368, 2018. [ DOI | arxiv | http ]

The Meaning of Memory Safety. Arthur Azevedo de Amorim, Cătălin Hrițcu, and Benjamin C. Pierce. In Proceedings of POST 2018, part of ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, pages 79--105, 2018. [ http ]

A methodology for micro-policies. Arthur Azevedo de Amorim. PhD thesis, University of Pennsylvania, 2017. [ .pdf ]

A semantic account of metric preservation. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 545--556, 2017. [ arxiv ]

Binding Operators for Nominal Sets. Arthur Azevedo de Amorim. Electr. Notes Theor. Comput. Sci., 325:3--27, 2016. [ http ]

A verified information-flow architecture. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hrițcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. Journal of Computer Security, 24(6):689--734, 2016. [ DOI | arxiv ]

Testing noninterference, quickly. Cătălin Hrițcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, and Dimitrios Vytiniotis. J. Funct. Program., 26:e4, 2016. [ DOI | arxiv ]

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. Yannis Juglaret, Cătălin Hrițcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016, pages 45--60, 2016. [ DOI | arxiv ]

Micro-Policies: Formally Verified, Tag-Based Security Monitors. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hrițcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015, pages 813--830, 2015. [ DOI | slides | full version ]

Really Natural Linear Indexed Type Checking. Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. In Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, IFL '14, Boston, MA, USA, October 1-3, 2014, pages 5:1--5:12, 2014. [ DOI | arxiv ]

A verified information-flow architecture. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hrițcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 165--178, 2014. [ DOI | slides ]

Testing noninterference, quickly. Cătălin Hrițcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 455--468, 2013. [ DOI ]

Students

• Dongyu Wu (PhD)
• Vivien Rindisbacher (BS)

Software

Deriving: A Coq library for automating the definition of class instances for inductive types.

Extensional Structures: A Coq library of finite data structures that support extensional equality.

Micro-policies: A programming model for tag-based security policies formalized in Coq.

Coq utils: A small library of Coq utilities, including a formalization of nominal sets.

Netter: A language for modeling and verifying probabilistic, stateful networks.

Taglierino: A bounded model checker for cryptographic protocols.