Email: shigoel at cs dot utexas dot eduDesk: GDC 7.814A
ACL2 Theorem Proving Group
____________________________________________________________________________________________________Home Classes Academic Activities Publications Personal
I came to the University of Texas at Austin as a Master's student
in Fall '10 but I switched to being a Ph.D. student in Spring '12.
I am a Research Assistant under
Prof. Warren A. Hunt, Jr
and use the ACL2
Theorem Prover --- the latest in the Boyer-Moore Family of Theorem
Provers --- to prove properties of systems that many people care
Currently, I am working on the specification of the X86 ISA in ACL2. For details about the motivations and goals of the project, see "X86 Specification in ACL2" and "Robust Reasoning Framework for Machine Code Verification".