Shilpi Goel

Shilpi Goel

About Me

I am a Formal Verification Engineer at Centaur Technology (since January 2017). I also maintain a formal model of the x86 ISA --- which started as my Ph.D. dissertation project.

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.

Publications

Alessandro Coglio and Shilpi Goel

Adding 32-bit Mode to the ACL2 Model of the x86 ISA

To appear in ACL2 Workshop, 2018


Shilpi Goel

The x86isa Books: Features, Usage, and Future Plans

In ACL2 Workshop, 2017

[Link]


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.

[Link]


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

[Link]


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

[Link]

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

[Link]

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

Abstract Stobjs and Their Application to ISA Modeling

In ACL2 Workshop, 2013

[Link]

Academic Activities

Program Co-Chair

2018

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


Local Arrangements Chair

2015

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


Webmaster

2013-2015

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