Welcome to my website! I am Hanna a fourth-year PhD student at Stanford University. I am adviced by Clark Barrett and part of the CENTAUR lab.

I am interested in Automated Reasoning and Formal Verification. Currently, I am working on reconstructing fine-grained proof certificates from the cvc5 SMT solver in the interactive theorem prover Isabelle.



  • Coming soon! Our tool paper on IsaRARE has been accepted to TACAS 24. IsaRARE is a tool that can transform rewrite rules written in the RARE language into Isabelle lemmas.