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.

News:

• Coming soon! Better integration of cvc5 into Isabelle should be available with the next release. We made a lot of changes so things will break. Please let me know if you get any SMT related errors, even if they concern veriT and z3.