I am a Formal Verification Engineer at Centaur Technology (joined in January, 2017). I also maintain a formal model of the x86 ISA --- which started as my Ph.D. dissertation project --- in my free time.
I graduated from UT CS with my Ph.D. in December, 2016 under the supervision of Prof. Warren A. Hunt, Jr. For my dissertation project, I worked on the formal analysis of x86 application and system programs via machine-code verification. I am the primary author of the x86isa library, which contains a formal and executable model of the x86 instruction-set architecture in ACL2. This model has been used to both simulate and formally verify x86 machine-code programs. The x86isa library is available from the ACL2+Community Books Github page.