About
My main research interest lies at the intersection between interactive theorem proving (ITP) and formal semantics of programming languages. As a member of the reactive system groups, I am using interactive theorem proving to verify complex properties of reactive programs, and to formalize the semantics of reactive programming languages. More precisely, I am actively working on the following topics:
- Trustworthy model-checking and bug finding
- Automated bug finding for Hyperproperties
- Interactive verification of Hyperproperties
- Mechanized semantics of reactive programming languages
More details on my research can be found on my personal page https://acorrenson.github.io.