I defended my Ph.D. in November 2016. I was supervised by 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 and its user/developer manual is available here.
For slides, papers, etc., related to my Ph.D. research, click here.