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 at Carnegie 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 Rocq proof assistant (previously known as Coq), and write about Rocq in my blog.
Email: arthur.aa@gmail.com
Office: GOL-3547
Current research
Cryptographic protocols
Cryptographic protocols such as TLS are crucial for securing communication over the Internet. Unfortunately, their design is tricky to get right, which often results in devastating attacks. We are currently developing a formalism that leverages recent advances in program verification (in particular, separation logic) to verify cryptographic protocols. These verified protocols can be combined with standard proofs of correctness to derive application-level specifications. For more information, check out our draft and accompanying Rocq formalization.
Compartmentalization
Low-level languages such as C and C++ are often seen as the gold standard for fast systems code, but their unsafe semantics often leads to simple bugs turning into critical vulnerabilities. Compartmentalization refers to a series of techniques for limiting the scope of such vulnerabilities, often leveraging process-based isolation, code instrumentation, or specialized hardware. We have been analyzing the formal guarantees of such compartmentalization techniques, and have applied them to develop SECOMP, the first formally verified realistic compartmentalizing compiler. If you want to learn more, check out our paper, available here.
News
February 2026 I will be teaching an introductory class on the Rocq proof assistant at the Oregon Programming Languages Summer School (OPLSS) in July.
November 2025 Our paper Cryptis: Cryptographic Reasoning in Separation Logic was selected to appear at POPL 2026.
March 2025 Our draft Cryptis: Cryptographic Reasoning in Separation Logic is out. The accompanying Rocq formalization is available here.
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.
Teaching
Current (Spring 2026) Topics in Languages and Tools (CSCI 749); Verification using proof assistants
Other classes at RIT
- Programming Language Concepts (CSCI 344); offered in the spring of 23 and 24.
- Programming Language Theory (CSCI 740); offered in the fall of 23, 24 and 25.
Other classes elsewhere
- Formal Proofs about Programs, CS 599 G1 (at Boston University, spring 22).
Recent Publications
Full list here. Check also my DBLP and Google Scholar pages.
Cryptis: Cryptographic Reasoning in Separation Logic. With Amal Ahmed and Marco Gaboardi. POPL 2026. [ DOI | http ]
Memory Safety: Uniqueness as Separation. With Pilar Selene Linares-Arévalo, Vincent Jackson, et al. APLAS 2025. [ DOI | http ]
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 ]
Students
I am fortunate to be currently advising the following amazing students at RIT:
- Dongyu Wu (PhD)
- Chandradeep Dey (PhD)
- Jeremy Stratton-Smith (PhD)
- Melwyn Saldanha (MS)
- Eloise Christian (MS)
- Klim Fedorchuk (MS)
- Tejas Gadwalkar (BS)
- Lyx Huston (BS)
- Andrew Cudzinovic (BS)
Besides official advising duties, I have also mentored and worked with many other students in various capacities. Here are some of them:
- Cheng Zheng (BU, PhD; currently at Worcester Polytechnic Institute (WPI))
- june wunder (BU, PhD)
- Vivien Rindisbacher (BU, BS; currently a PhD student at UCSD)
Software
Cryptis: An extension of the Iris separation logic for verifying cryptographic protocols.
Deriving: A Rocq library for automating the definition of class instances for inductive types.
Extensional Structures: A Rocq library of finite data structures that support extensional equality.
Micro-policies: A programming model for tag-based security policies formalized in Rocq.
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.