Arthur Azevedo de Amorim

Arthur Azevedo de Amorim is an Assistant Professor in the Department of Computer Science at the Rochester Institute of Technology (RIT), part of the College of Computing and Information Sciences. His research lies at the intersection of programming languages, formal verification, and software security.

• Ph.D., University of Pennsylvania (advised by Benjamin Pierce and Cătălin Hrițcu)
• Postdoctoral Fellow, Boston University and Carnegie Mellon University
• B.S., Unicamp and Polytechnique

His research focuses on enhancing software security and reliability through formal methods, particularly using formal verification, programming languages, and type systems. Key areas include cryptographic protocols, where he develops formalisms based on separation logic to verify protocols like TLS, and compartmentalization, where he analyzes and implements formally verified techniques to limit the impact of vulnerabilities in low-level code. His work includes the development of SECOMP, the first formally verified realistic compartmentalizing compiler.

His recent publications span top conferences such as POPL, CCS, ESOP, and ICALP, reflecting a strong trend toward foundational work in program logics, secure compilation, and type-based security. His research often involves deep formalization in the Coq proof assistant, and he contributes to the formal methods community through open-source tools and educational resources like the Software Foundations textbook.

He is actively involved in academic service, having served on program committees for POPL, ICFP, PLDI, and others. He mentors several graduate and undergraduate students at RIT and has previously mentored researchers at Boston University.

Notable software contributions include:

• Cryptis: Extension of Iris separation logic for cryptographic protocols
• Deriving: Coq library for automating class instances
• Extensional Structures: Coq library for finite data structures
• Netter: Language for probabilistic network modeling