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.

Academic Service

2022: Program Committee Member

Computer-Aided Verification: Artifact Evaluation (CAV-AE22)

2022: Program and Steering Committee Member

17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2022)

2021: Program Committee Member

Certified Programs and Proofs (CPP 2021)

2020: Program and Steering Committee Member

16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2020)

2019: Program Committee Member

10th International Conference on Interactive Theorem Proving (ITP-2019)

2018: Co-Chair and Program Committee Member

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

2015: Local Arrangements Chair

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

2013-2015: Webmaster

Formal Methods in Computer-Aided Design Conferences (FMCAD)

Misc. Projects

I have had fun working on the following somewhat recent projects.

Bigmem

A 2^64-byte memory model that is logically a record but provides array-like performance during execution

Exld

A parser for ELF and Mach-O files in ACL2

Instant Run-Off Voting

An ACL2 formalization of an instant-runoff voting scheme and proofs of some fairness criteria

Presented as an ACL2-2018 Rump Session Talk [Slides]

This project was particularly fun because my partner, Mayank Manjrekar, and I collaborated on it!