-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
284 lines (234 loc) · 11.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
<!DOCTYPE html>
<html>
<head>
<title>Shilpi Goel</title>
<meta name="viewport" content="width=device-width"/>
<meta name="description" content="Shilpi Goel."/>
<meta charset="UTF-8">
<link type="text/css" rel="stylesheet" href="style.css">
<!-- <link href='http://fonts.googleapis.com/css?family=Rokkitt:400,700|Lato:400,300' --
-- rel='stylesheet' type='text/css'> -->
<link rel="icon" href="favicon.ico">
<!--[if lt IE 9]>
<script src="//html5shiv.googlecode.com/svn/trunk/html5.js"></script>
<![endif]-->
</head>
<body id="top">
<div id="cv">
<div class="mainDetails">
<div id="headshot">
<a href="index.html"><img src="shilpi_goel.jpg" alt="Shilpi Goel" /></a>
</div>
<div id="name">
<h1 style="color:White;">Shilpi Goel</h1>
<ul>
<li style="color:White;">Formal Methods Practitioner</li>
<li style="color:White;">Software and Hardware Analysis</li>
</ul>
</div>
<div id="contactDetails">
<ul>
<li><tt><a href="https://github.com/shigoel">https://github.com/shigoel</a></tt></li>
<li><tt><a href="https://www.linkedin.com/in/shilpigoel">https://www.linkedin.com/in/shilpigoel</a></tt></li>
</ul>
</div>
<div class="clear"></div>
</div>
<div id="mainArea">
<section>
<article>
<!-- <div class="sectionTitle"> -->
<!-- <h1>About Me</h1> -->
<!-- </div> -->
<div class="sectionContent">
<p>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.</p>
<p>I graduated from The University of Texas at Austin
with my Ph.D. (Computer Science) in 2016 under the
supervision of
<a href="https://www.cs.utexas.edu/users/hunt">Warren
A. Hunt, Jr.</a> 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 <tt><a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____X86ISA">x86isa</a></tt>
library, which contains a formal and executable model of
(a subset of) the x86 ISA
in <a href="https://www.cs.utexas.edu/users/moore/acl2">ACL2</a>. The <tt>x86isa</tt>
library is available from
the <a href="https://github.com/acl2/acl2/tree/master/books/projects/x86isa">ACL2+Community
Books Github page</a>.</p>
</div>
</article>
<div class="clear"></div>
</section>
<section>
<div class="sectionTitle">
<h1>Papers <a itemprop="sameAs" content="https://orcid.org/0000-0001-8037-0201" href="https://orcid.org/0000-0001-8037-0201" target="orcid.widget" rel="me noopener noreferrer" style="vertical-align:top;"><img src="https://orcid.org/sites/default/files/images/orcid_16x16.png" style="width:1em;margin-right:.5em;" alt="ORCID iD icon"></a></h1>
</div>
<br>
<div class="sectionContent">
<article>
<p class="subDetails">Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords.</p>
<p class="subDetailsNormal"><a href="https://link.springer.com/chapter/10.1007%2F978-3-030-81685-8_2">Balancing Automation and Control for Formal Verification of Microprocessors</a></p>
<p class="subDetailsNormal">In the proceedings of the 33rd International Conference on Computer-Aided Verification (CAV), 2021.</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords.</p>
<p class="subDetailsNormal"><a href="https://dl.acm.org/doi/10.1145/3372885.3373811">Verifying x86 Instruction Implementations</a> <a href="talks/CPP-2020.pdf" class="slides">[Slides]</a></p>
<p class="subDetailsNormal">In the proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2020.</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel and Rob Sumners.</p>
<p class="subDetailsNormal"><a href="https://www.cl.cam.ac.uk/~jrh13/spisa19/paper_08.pdf">Using x86isa for Microcode Verification</a> <a href="talks/SpISA-2019.pdf" class="slides">[Slides]</a></p>
<p class="subDetailsNormal">In the Workshop on Instruction Set Architecture Specification (SpISA), 2019.</p>
</article>
<br>
<article>
<p class="subDetails">Alessandro Coglio and Shilpi Goel</p>
<p class="subDetailsNormal"><a href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22018.6">Adding 32-bit Mode to the ACL2 Model of the x86 ISA</a> </p>
<p class="subDetailsNormal">In the Fifteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2018.</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel</p>
<p class="subDetailsNormal"><a href="https://arxiv.org/abs/1705.01225v1">The <tt>x86isa</tt> Books: Features, Usage, and Future Plans</a>
<a href="talks/ACL2-2017.pdf" class="slides">[Slides]</a></p>
<p class="subDetailsNormal">In the Fourteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2017</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel</p>
<p class="subDetailsNormal"><a href="http://hdl.handle.net/2152/46437">Formal Verification of
Application and System Programs Based on a Validated x86 ISA Model</a>
<a href="talks/Defense-Talk.pdf" class="slides">[Defense Slides]</a>
</p>
<p class="subDetailsNormal">
<a href="talks/Proposal-Talk.pdf" class="slides">[Proposal Slides]</a>
<a href="talks/RPE-Talk.pdf" class="slides">[Research Prep Exam Slides]</a>
</p>
<p class="subDetailsNormal">{Ph.D. Dissertation} Department of Computer Science, The University of Texas at Austin. 2016.</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann</p>
<p class="subDetailsNormal"><a href="https://link.springer.com/chapter/10.1007%2F978-3-319-48628-4_8">Engineering a Formal, Executable x86 ISA Simulator for Software Verification</a></p>
<p class="subDetailsNormal">{Book Chapter} In Provably Correct Systems (ProCoS), 2017.</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel, Warren A. Hunt, Jr., Matt Kaufmann, and Soumava Ghosh</p>
<p class="subDetailsNormal"><a class="subDetailsNormal" href="http://dx.doi.org/10.1109/FMCAD.2014.6987600">Simulation and Formal Verification of x86 Machine-Code Programs That Make System Calls</a>
<a href="talks/FMCAD-2014.pdf" class="slides">[Slides]</a></p>
<p class="subDetailsNormal">In Formal Methods in Computer-Aided Design (FMCAD), 2014.</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel and Warren A. Hunt, Jr.</p>
<p class="subDetailsNormal"><a class="subDetailsNormal" href="http://dx.doi.org/10.1007/978-3-642-54108-7_12">Automated Code Proofs on a Formal Model of the x86</a>
<a href="talks/VSTTE-2013.pdf" class="slides">[Slides]</a></p>
<p class="subDetailsNormal">In Verified Software:
Theories, Tools, Experiments (VSTTE), 2013.</p>
</article>
<br>
<article>
<p class="subDetails">Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann</p>
<p class="subDetailsNormal"><a class="subDetailsNormal" href="http://arxiv.org/abs/1304.7858">Abstract Stobjs and Their Application to ISA Modeling</a>
<a href="talks/ACL2-2013.pdf" class="slides">[Slides]</a></p>
<p class="subDetailsNormal">In the Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2013.</p>
</article>
<br>
</div>
<div class="clear"></div>
</section>
<!--
<section>
<div class="sectionTitle">
<h1>Academic Service</h1>
</div>
<br>
<div class="sectionContent">
<article>
<h3>2025: Program Committee Member</h3>
<p class="tab subDetails">Design Automation and Test in Europe; Track D3 Formal methods and verification
(<a href="">DATE 2025</a>)</p>
</article>
<article>
<h3>2025: Program Committee Member</h3>
<p class="tab subDetails">19th International Workshop
on the ACL2 Theorem Prover and Its Applications
(<a href="https://www.cs.utexas.edu/users/moore/acl2/workshop-2023/index.html">ACL2 2025</a>)</p>
</article>
<article>
<h3>2023: Program Committee Member</h3>
<p class="tab subDetails">18th International Workshop
on the ACL2 Theorem Prover and Its Applications
(<a href="https://www.cs.utexas.edu/users/moore/acl2/workshop-2023/index.html">ACL2 2023</a>)</p>
</article>
<article>
<h3>2022: Program and Steering Committee Member</h3>
<p class="tab subDetails">17th International Workshop
on the ACL2 Theorem Prover and Its Applications
(<a href="https://www.cs.utexas.edu/users/moore/acl2/workshop-2022/index.html">ACL2 2022</a>)</p>
</article>
<article>
<h3>2021: Program Committee Member</h3>
<p class="tab subDetails">Certified Programs and Proofs
(<a href="https://popl21.sigplan.org/home/CPP-2021?">CPP 2021</a>)</p>
</article>
<article>
<h3>2020: Program and Steering Committee Member</h3>
<p class="tab subDetails">16th International Workshop
on the ACL2 Theorem Prover and Its Applications
(<a href="http://acl2-2020.info/">ACL2 2020</a>)</p>
</article>
<article>
<h3>2019: Program Committee Member</h3>
<p class="tab subDetails">10th International
Conference on Interactive Theorem Proving
(<a href="https://itp19.cecs.pdx.edu/">ITP-2019</a>)</p>
</article>
<article>
<h3>2018: Co-Chair and Program Committee Member</h3>
<p class="tab subDetails">15th International Workshop
on the ACL2 Theorem Prover and Its Applications
(<a href="http://www.cs.utexas.edu/users/moore/acl2/workshop-2018/index.html">ACL2-2018</a>)</p>
</article>
<article>
<h3>2015: Local Arrangements Chair</h3>
<p class="tab subDetails">Formal Methods in Computer-Aided Design
(<a href="http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD15/index.shtml">FMCAD'15</a>)</p>
</article>
<article>
<h3>2013-2015: Webmaster</h3>
<p class="tab subDetails">Formal Methods in Computer-Aided Design Conferences
(<a href="http://www.cs.utexas.edu/users/hunt/FMCAD/">FMCAD</a>)</p>
</article>
<br>
</div>
<div class="clear"></div>
</section>
-->
</div>
</div>
<script type="text/javascript">
var gaJsHost = (("https:" == document.location.protocol) ? "https://ssl." : "http://www.");
document.write(unescape("%3Cscript src='" + gaJsHost + "google-analytics.com/ga.js' type='text/javascript'%3E%3C/script%3E"));
</script>
<script type="text/javascript">
var pageTracker = _gat._getTracker("UA-3753241-1");
pageTracker._initData();
pageTracker._trackPageview();
</script>
</body>
<!-- <footer> -->
<!-- <p>Shilpi Goel <br> Website template adapted -->
<!-- from <a href="http://www.thomashardy.me.uk/free-responsive-html-css3-cv-template">Thomas -->
<!-- Hardy's pages</a></p> -->
<!-- </footer> -->
</html>