Broadly speaking, I am interested in the intersection of mathematics and computer science. More specifically, I am interested in formally verifying mathematical results and algorithms that have safety-critical applications. I typically work in the theorem prover Isabelle/HOL; you can find my AFP entries here.
Broadly speaking, I am interested in the intersection of mathematics and computer science. More specifically, I am interested in formally verifying mathematical results and algorithms that have safety-critical applications. I typically work in the theorem prover Isabelle/HOL; you can find my AFP entries here.
In grad school, I focused on formalizing algorithms for real quantifier elimination in Isabelle/HOL (my thesis topic). I also considered other topics that are relevant to the formal verification of cyber-physical systems (CPS): namely, efficient invariant generation and modeling (specifically, how to write models of CPS that build an awareness of physics into logic). My graduate school work was generously supported by an NSF Graduate Research Fellowship.
In grad school, I focused on formalizing algorithms for real quantifier elimination in Isabelle/HOL (my thesis topic). I also considered other topics that are relevant to the formal verification of cyber-physical systems (CPS): namely, efficient invariant generation and modeling (specifically, how to write models of CPS that build an awareness of physics into logic). My graduate school work was generously supported by an NSF Graduate Research Fellowship.
Prior to graduate school, I did research in various areas of mathematics. My Erdős number is 3.
Prior to graduate school, I did research in various areas of mathematics. My Erdős number is 3.