Shilpi Goel

Shilpi Goel

About Me

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.


Shilpi Goel

The x86isa Books: Features, Usage, and Future Plans

In ACL2 Workshop, 2017


Shilpi Goel

Formal Verification of Application and System Programs Based on a Validated x86 ISA Model

Ph.D. Dissertation, Department of Computer Science, The University of Texas at Austin. 2016.


Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann

Engineering a Formal, Executable x86 ISA Simulator for Software Verification

In Provably Correct Systems (ProCoS), 2017


Shilpi Goel, Warren A. Hunt, Jr., Matt Kaufmann, and Soumava Ghosh

Simulation and Formal Verification of x86 Machine-Code Programs That Make System Calls

In Formal Methods in Computer-Aided Design (FMCAD), 2014


Shilpi Goel and Warren A. Hunt, Jr.

Automated Code Proofs on a Formal Model of the x86

In Verified Software: Theories, Tools, Experiments (VSTTE), 2013


Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann

Abstract Stobjs and Their Application to ISA Modeling

In ACL2 Workshop, 2013


Academic Activities

Program Co-Chair


15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2018)

Local Arrangements Chair


Conference: Formal Methods in Computer-Aided Design (FMCAD'15)



Conference: Formal Methods in Computer-Aided Design (FMCAD)