Shilpi Goel

Formal Methods Practitioner
Software and Hardware Analysis

I am a Senior Applied Scientist in the Automated Reasoning Group at Amazon Web Services. Previously, I was a Formal Verification Engineer at Intel Corporation and before that, at Centaur Technology.

I graduated from The University of Texas at Austin with my Ph.D. (Computer Science) in 2016 under the supervision of Warren A. Hunt, Jr. For my dissertation project, I worked on developing tools and techniques to enable 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 (a subset of) the x86 ISA in ACL2. The x86isa library is available from the ACL2+Community Books Github page.

Papers

Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords.

Balancing Automation and Control for Formal Verification of Microprocessors

In the proceedings of the 33rd International Conference on Computer-Aided Verification (CAV), 2021.

Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords.

Verifying x86 Instruction Implementations [Slides]

In the proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2020.

Shilpi Goel and Rob Sumners.

Using x86isa for Microcode Verification [Slides]

In the Workshop on Instruction Set Architecture Specification (SpISA), 2019.

Alessandro Coglio and Shilpi Goel

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

In the Fifteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2018.

Shilpi Goel

The x86isa Books: Features, Usage, and Future Plans [Slides]

In the Fourteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2017

Shilpi Goel

Formal Verification of Application and System Programs Based on a Validated x86 ISA Model [Defense Slides]

[Proposal Slides] [Research Prep Exam Slides]

{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

{Book Chapter} 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 [Slides]

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 [Slides]

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 [Slides]

In the Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2013.