Shilpi Goel

Shilpi Goel

  • Ph.D. Candidate
  • Department of Computer Science
  • The University of Texas at Austin

About Me

I am a Ph.D. Candidate in the ACL2 Theorem Proving Group, and my advisor is Prof. Warren A. Hunt, Jr.

I am working 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 and its user/developer manual is available here.


Doctor of Philosophy: Computer Science

August 2010 - August 2016 (Expected)
The University of Texas at Austin, USA

More Info...

Bachelor of Technology: Computer Science and Engineering

August 2006 - August 2010
Amity University, India

More Info...

Work Experience

Formal Verification Engineer Intern at Centaur Technology

May 2015 - August 2015

May 2014 - December 2014

Formal Verification of Microprocessor Design (RTL-Level Design in Verilog/SystemVerilog) using ACL2 and automatic tools like SAT solvers

Teaching Assistant at The University of Texas at Austin

August 2010 - December 2010

Undergraduate Computer Architecture


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

Engineering a Formal, Executable x86 ISA Simulator for Software Verification

To appear in Provably Correct Software (ProCoS), 2015

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

Local Arrangements Chair


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



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

Key Skills

  • ACL2/Lisp
  • x86 assembly
  • C
  • Python
  • Dynamic program instrumentation/debugging using GDB and Pintool
  • Microprocessor modeling and specification
  • Developing co-simulation frameworks

Selected Graduate Coursework

Recursion and Induction, Introduction to Mathematical Logic, Programming Languages, Combinatorics and Graph Theory, Logic-Based Artificial Intelligence, Formal Semantics and Verification, Distributed Computing, Practical SAT Solving