-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcv.html
380 lines (364 loc) · 21 KB
/
cv.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
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="author" content="Emina Torlak">
<meta name="description" content="Emina Torlak's CV">
<meta name="keywords" content="Rosette, Kodkod, Cedar">
<title>Emina Torlak: CV</title>
<link rel="stylesheet" href="css/cv.css">
</head>
<body>
<header>
<h1>Emina Torlak</h1>
<div>
<a href="https://emina.github.io/">https://emina.github.io/</a>
</div>
</header>
<h2 id="Education">Education</h2>
<table>
<tr>
<td>Massachusetts Institute of Technology, <a href="#kodkod:phd09">Ph.D.</a>, Computer Science</td>
<td>2009</td>
</tr>
<tr>
<td>Massachusetts Institute of Technology, <a href="#alloy-types:meng04">M.Eng.</a>, Computer Science</td>
<td>2004</td>
</tr>
<tr>
<td>Massachusetts Institute of Technology, B.Sc., Computer Science</td>
<td>2003</td>
</tr>
</table>
<h2 id="Employment">Employment</h2>
<table>
<tr>
<td>Senior Principal Applied Scientist, Amazon Web Services</td>
<td>2021–</td>
</tr>
<tr>
<td>Affiliate Professor, Allen School, University of Washington</td>
<td>2024–</td>
</tr>
<tr>
<td>Associate Professor, Allen School, University of Washington</td>
<td>2018–2023</td>
</tr>
<tr>
<td>Assistant Professor, Allen School, University of Washington</td>
<td>2014–2018</td>
</tr>
<tr>
<td>Research Engineer, EECS, University of California Berkeley</td>
<td>2012–2014</td>
</tr>
<tr>
<td>Senior Computer Scientist, LogicBlox, Inc.</td>
<td>2011</td>
</tr>
<tr>
<td>Research Staff Member, IBM Research</td>
<td>2008–2010</td>
</tr>
</table>
<h2 id="Awards">Awards</h2>
<table>
<tr>
<td><a href="https://www.sigplan.org/Awards/Milner/">Robin Milner Young Researcher Award</a></td>
<td>2021</td>
</tr>
<tr>
<td><a href="https://www.amazon.science/research-awards/recipients/emina-torlak">Amazon Research Award</a></td>
<td>2020</td>
</tr>
<tr>
<td>ASE Distinguished Paper Award [<a href="#solar:ase20">9</a>]</td>
<td>2020</td>
</tr>
<tr>
<td>SOSP Best Paper and Distinguished Artifact Awards [<a href="#serval:sosp19">12</a>]</td>
<td>2019</td>
</tr>
<tr>
<td>OOPSLA Distinguished Artifact Award [<a href="#sympro:oopsla18">14</a>]</td>
<td>2018</td>
</tr>
<tr>
<td>ICSE Distinguished Paper Award [<a href="#daisy:icse18">16</a>]</td>
<td>2018</td>
</tr>
<tr>
<td><a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=1651225">NSF CAREER Award</a></td>
<td>2017</td>
</tr>
<tr>
<td><a href="https://sloan.org/fellows-database?page=87">Sloan Research Fellow</a></td>
<td>2016</td>
</tr>
<tr>
<td><a href="http://www.2001.ecoop.org/Dahl-Nygaard/">The AITO Dahl-Nygaard Junior Prize</a></td>
<td>2016</td>
</tr>
<tr>
<td>OSDI Best Paper Award [<a href="#yggy:osdi16">25</a>]</td>
<td>2016</td>
</tr>
<tr>
<td>FSE Distinguished Paper Award [<a href="#testblox:fse12">43</a>]</td>
<td>2012</td>
</tr>
</table>
<h2 id="Publications">Publications</h2>
<h3 id="Conference_and_Journal_Papers">Conference and Journal Papers</h3>
<ol>
<li id="vgd:fse24">Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, and Andrew Wells. <a href="https://doi.org/10.1145/3663529.3663854">How We Built Cedar: A Verification-Guided Approach</a>. FSE, 2024.</li>
<li id="cedar:oopsla24">Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew Wells. <a href="https://dl.acm.org/doi/10.1145/3649835">Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization</a>. OOPSLA, 2024.</li>
<li id="prettyprinter:oopsla23">Sorawee Porncharoenwase, Justin Pombrio, and Emina Torlak. <a href="https://dl.acm.org/doi/abs/10.1145/3622837">A pretty expressive printer</a>. OOPSLA, 2023.</li>
<li id="depsynth:ecoop23">Jacob Van Geffen, Xi Wang, Emina Torlak, and James Bornholt. <a href="https://doi.org/10.4230/LIPIcs.ECOOP.2023.35">Synthesis-Aided Crash Consistency for Storage Systems</a>. ECOOP, 2023.</li>
<li id="xdsmith:issta22">Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, and Emina Torlak. <a href="https://dl.acm.org/doi/abs/10.1145/3533767.3534382">Testing Dafny (experience paper)</a>. ISSTA, 2022.</li>
<li id="rosette:popl22">Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak. <a href="https://doi.org/10.1145/3498709">A formal foundation for symbolic evaluation with merging</a>. POPL, 2022.</li>
<li id="jitterbug:osdi20">Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. <a href="https://www.usenix.org/conference/osdi20/presentation/nelson">Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel</a>. OSDI, 2020.</li>
<li id="ni:sigops20">Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. <a href="https://dl.acm.org/doi/10.1145/3421473.3421478">Noninterference specifications for secure systems</a>. ACM SIGOPS Operating Systems Review, 2020.</li>
<li id="solar:ase20">Yu Feng, Emina Torlak, and Rastislav Bodik. <a href="https://dl.acm.org/doi/10.1145/3324884.3416646">Summary-Based Symbolic Evaluation for Smart Contracts</a>. ASE, 2020. <strong>Distinguished Paper Award</strong>.</li>
<li id="jitsynth:cav20">Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak. <a href="https://link.springer.com/chapter/10.1007/978-3-030-53291-8_29">Synthesizing JIT Compilers for In-Kernel DSLs</a>. CAV, 2020.</li>
<li id="symfix:vmcai20">Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. <a href="https://link.springer.com/chapter/10.1007/978-3-030-39322-9_3">Fixing Code That Explodes Under Symbolic Evaluation</a>. VMCAI, 2020.</li>
<li id="serval:sosp19">Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. <a href="https://dl.acm.org/doi/10.1145/3341301.3359641">Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval</a>. SOSP, 2019. <strong>Best Paper and Distinguished Artifact Awards</strong>.</li>
<li id="swizzle:asplos19">Phitchaya Mangpo Phothilimthana, Archibald Samuel Elliott, An Wang, Abhinav Jangda, Bastian Hagedorn, Henrik Barthels, Samuel J. Kaufman, Vinod Grover, Emina Torlak, and Rastislav Bodik. <a href="https://dl.acm.org/doi/10.1145/3297858.3304059">Swizzle Inventor: Data Movement Synthesis for GPU Kernels</a>. ASPLOS, 2019.</li>
<li id="sympro:oopsla18">James Bornholt and Emina Torlak. <a href="https://dl.acm.org/citation.cfm?id=3276519">Finding Code That Explodes Under Symbolic Evaluation</a>. OOPSLA, 2018. <strong>Distinguished Artifact Award</strong>.</li>
<li id="nickel:osdi18">Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. <a href="https://www.usenix.org/conference/osdi18/presentation/sigurbjarnarson">Nickel: A Framework for Design and Verification of Information Flow Control Systems</a>. OSDI, 2018.</li>
<li id="daisy:icse18">Calvin Loncaric, Michael D. Ernst, and Emina Torlak. <a href="https://dl.acm.org/citation.cfm?id=3180211">Generalized Data Structure Synthesis</a>. ICSE, 2018. <strong>Distinguished Paper Award</strong>.</li>
<li id="rulesy:vmcai18">Eric Butler, Emina Torlak, and Zoran Popovic. <a href="https://link.springer.com/chapter/10.1007%2F978-3-319-73721-8_7">A Framework for Computer-Aided Design of Educational Domain Models</a>. VMCAI, 2018.</li>
<li id="rtr:vmcai18">Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeff Foster, and Emina Torlak. <a href="https://link.springer.com/chapter/10.1007%2F978-3-319-73721-8_13">Refinement Types for Ruby</a>. VMCAI, 2018.</li>
<li id="typedrosette:popl18">Stephen Chang, Alex Knauth, and Emina Torlak. <a href="https://dl.acm.org/citation.cfm?doid=3158128">Symbolic Types for Lenient Symbolic Execution</a>. POPL, 2018.</li>
<li id="neutrons:icalepcs17">Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, and Emina Torlak. <a href="https://doi.org/10.18429/JACoW-ICALEPCS2017-TUDPL02">Automatic Formal Verification for EPICS</a>. ICALEPCS, 2017.</li>
<li id="hyperkernel:sosp17">Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. <a href="https://dl.acm.org/authorize?N47250">Hyperkernel: Push-Button Verification of an OS Kernel</a>. SOSP, 2017.</li>
<li id="nonograms:fdg17">Eric Butler, Emina Torlak, and Zoran Popovic. <a href="http://dl.acm.org/citation.cfm?id=3102084">Synthesizing Interpretable Strategies for Solving Puzzle Games</a>. FDG, 2017.</li>
<li id="memsynth:pldi17">James Bornholt and Emina Torlak. <a href="http://dl.acm.org/citation.cfm?id=3062353">Synthesizing Memory Models from Framework Sketches and Litmus Tests</a>. PLDI, 2017.</li>
<li id="spacesearch:icfp17">Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock. <a href="http://dl.acm.org/citation.cfm?id=3136534.3110269">SpaceSearch: A Library for Building and Verifying Solver-Aided Tools</a>. ICFP, 2017.</li>
<li id="yggy:osdi16">Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. <a href="https://www.usenix.org/conference/osdi16/technical-sessions/presentation/sigurbjarnarson">Push-Button Verification of File Systems via Crash Refinement</a>. OSDI, 2016. <strong>Best Paper Award</strong>.</li>
<li id="cassius:oopsla16">Pavel Panchekha and Emina Torlak. <a href="http://dl.acm.org/citation.cfm?id=2984010">Automated Reasoning for Web Page Layout</a>. OOPSLA, 2016.</li>
<li id="bagpipe:oopsla16">Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. <a href="http://dl.acm.org/citation.cfm?id=2984012">Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver</a>. OOPSLA, 2016.</li>
<li id="neutrons:cav16">Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky. <a href="http://dx.doi.org/10.1007/978-3-319-41540-6_2">Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers</a>. CAV, 2016.</li>
<li id="rulesynth:its16">Eric Butler, Emina Torlak, and Zoran Popovic. <a href="http://dx.doi.org/10.1007/978-3-319-39583-8_36">A Framework for Parameterized Design of Rule Systems Applied to Algebra</a>. ITS, 2016.</li>
<li id="cozy:pldi16">Calvin Loncaric, Emina Torlak, and Michael D. Ernst. <a href="http://dl.acm.org/citation.cfm?id=2908122">Fast synthesis of fast collections</a>. PLDI, 2016.</li>
<li id="ferrite:asplos16">James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. <a href="http://dl.acm.org/citation.cfm?id=2872406">Specifying and Checking File System Crash-Consistency Models</a>. ASPLOS, 2016.</li>
<li id="synapse:popl16">James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. <a href="http://dl.acm.org/citation.cfm?id=2837666">Optimizing Synthesis with Metasketches</a>. POPL, 2016.</li>
<li id="lpd:onward15">Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler. <a href="http://dl.acm.org/citation.cfm?id=2814235">Toward Tool Support for Interactive Synthesis</a>. Onward!, 2015.</li>
<li id="crust:ase15">John Toman, Stuart Pernsteiner, and Emina Torlak. <a href="http://dl.acm.org/citation.cfm?id=2916213">CRust: A Bounded Verifier for Rust</a>. ASE, 2015.</li>
<li id="neutrons:snapl15">Michael Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang. <a href="http://drops.dagstuhl.de/opus/volltexte/2015/5020/">Toward a Dependability Case Language and Workflow for a Radiation Therapy System</a>. SNAPL, 2015.</li>
<li id="sygus:nato15">Rajeev Alur, Rastislav Bodik, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. <a href="http://ebooks.iospress.nl/publication/39188">Syntax-Guided Synthesis</a>. Dependable Software Systems Engineering, 2015.</li>
<li id="rosette:pldi14">Emina Torlak and Rastislav Bodik. <a href="http://dl.acm.org/citation.cfm?id=2594340">A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages</a>. PLDI, 2014.</li>
<li id="whatgives:vstte14">Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, and Satish Chandra. <a href="http://link.springer.com/chapter/10.1007%2F978-3-319-12154-3_17">What Gives?: A Hybrid Algorithm for Error Trace Explanation</a>. VSTTE, 2014.</li>
<li id="rosette:onward13">Emina Torlak and Rastislav Bodik. <a href="http://dl.acm.org/citation.cfm?id=2509586">Growing Solver-Aided Languages with Rosette</a>. Onward!, 2013.</li>
<li id="sygus:fmcad13">Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. <a href="https://ieeexplore.ieee.org/document/6679385">Syntax-Guided Synthesis</a>. FMCAD, 2013.</li>
<li id="alloy-apps:mscs13">Emina Torlak, Mana Taghdiri, Greg Dennis, and Joseph Near. <a href="http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=8951488">Applications and Extensions of Alloy: Past, Present, and Future</a>. Mathematical Structures in Computer Science, 2013.</li>
<li id="synth-tutorial:cav12">Rastislav Bodik and Emina Torlak. <a href="https://link.springer.com/chapter/10.1007/978-3-642-31424-7_3">Synthesizing Programs with Constraint Solvers (Invited Tutorial)</a>. CAV, 2012.</li>
<li id="testblox:fse12">Emina Torlak. <a href="http://dl.acm.org/citation.cfm?doid=2393596.2393637">Scalable test data generation from multidimensional models</a>. FSE, 2012. <strong>Distinguished Paper Award</strong>.</li>
<li id="angelina:icse11">Satish Chandra, Emina Torlak, Shaon Barman, and Rastislav Bodik. <a href="http://portal.acm.org/citation.cfm?doid=1985793.1985811">Angelic Debugging</a>. ICSE, 2011.</li>
<li id="refactoring:ecoop10">Max Schaefer, Julian Dolby, Manu Sridharan, Emina Torlak, and Frank Tip. <a href="http://www.springerlink.com/content/a0712w6186452717/">Correct Refactoring of Concurrent Java Code</a>. ECOOP, 2010.</li>
<li id="memsat:pldi10">Emina Torlak, Mandana Vaziri, and Julian Dolby. <a href="http://portal.acm.org/citation.cfm?doid=1806596.1806635">MemSAT: Checking Axiomatic Specifications of Memory Models</a>. PLDI, 2010.</li>
<li id="tracker:icse10">Emina Torlak and Satish Chandra. <a href="http://portal.acm.org/citation.cfm?doid=1806799.1806876">Effective interprocedural resource leak detection</a>. ICSE, 2010.</li>
<li id="kodkod:fm08">Emina Torlak, Felix Sheng-Ho Chang, and Daniel Jackson. <a href="http://www.springerlink.com/content/y17x1p3qw4550320/">Finding Minimal Unsatisfiable Cores of Declarative Specifications</a>. FM, 2008.</li>
<li id="cpufs:tissec08">Blaise Gassend, Marten Van Dijk, Dwaine Clarke, Emina Torlak, Srinivas Devadas, and Pim Tuyls. <a href="http://portal.acm.org/citation.cfm?doid=1284680.1284683">Controlled physical random functions and applications</a>. ACM Transactions on Information and System Security, 2008.</li>
<li id="kodkod:tacas07">Emina Torlak and Daniel Jackson. <a href="http://www.springerlink.com/content/d7768253121210g3/">Kodkod: A Relational Model Finder</a>. TACAS, 2007.</li>
<li id="atomization:issta04">Jonathan Edwards, Daniel Jackson, Emina Torlak, and Vincent Yeung. <a href="http://portal.acm.org/citation.cfm?doid=1007512.1007544">Faster constraint solving with subtypes</a>. ISSTA, 2004.</li>
<li id="alloy-types:fse04">Jonathan Edwards, Daniel Jackson, and Emina Torlak. <a href="http://portal.acm.org/citation.cfm?doid=1029894.1029921">A type system for object models</a>. FSE, 2004.</li>
</ol>
<h3 id="Patents_and_Theses">Patents and Theses</h3>
<ol>
<li id="angelina:patent12">Shaon K. Barman, Satish Chandra, and Emina Torlak. <a href="https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/8645761">Precise fault localization</a>. U.S. Patent Application No. 13/006,126, Publication No. US 2012/0185731 A1, 2012.</li>
<li id="refactoring:patent11">Julian Dolby, Max Schaefer, Manu Sridharan, Frank Tip, and Emina Torlak. <a href="https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/8689191">Correct Refactoring of Concurrent Software</a>. U.S. Patent Application No. 12/718,648, Publication No. US 2011/0219361 A1, 2011.</li>
<li id="memsat:patent11">Julian Dolby, Emina Torlak, and Mandana Vaziri. <a href="https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/20110113285">System and Method for Debugging Memory Consistency Models</a>. U.S. Patent Application No. 12/615,657, Publication No. US 2011/0113285 A1, 2011.</li>
<li id="tracker:patent11">Satish Chandra and Emina Torlak. <a href="https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/8689180">Systems and Methods for Resource Leak Detection</a>. U.S. Patent Application No. 12/611,561, Publication No. US 2011/0107297 A1, 2011.</li>
<li id="kodkod:phd09">Emina Torlak. <a href="http://portal.acm.org/citation.cfm?id=1713778&coll=DL&dl=GUIDE&CFID=28292589&CFTOKEN=69712818">A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications</a>. Ph.D. thesis, MIT, 2009.</li>
<li id="alloy-types:meng04">Emina Torlak. <a href="https://dspace.mit.edu/handle/1721.1/18012">Subtyping in Alloy</a>. Masters thesis, MIT, 2004.</li>
</ol>
<h2 id="Service">Service</h2>
<table>
<tr>
<td>PLDI, <strong>Area Chair</strong></td>
<td>2024</td>
</tr>
<tr>
<td>The Dahl–Nygaard Prize Committee, Member</td>
<td>2024</td>
</tr>
<tr>
<td>POPL, <strong>Associate Chair</strong></td>
<td>2024</td>
</tr>
<tr>
<td>PLDI, <strong>Steering Committee</strong></td>
<td>2018–2023</td>
</tr>
<tr>
<td>PLDI, <strong>Program Chair</strong></td>
<td>2020</td>
</tr>
<tr>
<td>SPLASH, <strong>Steering Committee</strong></td>
<td>2018–2020</td>
</tr>
<tr>
<td>PLDI, Program Committee</td>
<td>2019</td>
</tr>
<tr>
<td>OOPSLA, Review Committee</td>
<td>2019</td>
</tr>
<tr>
<td>The Future of Alloy Workshop, Program Co-Chair</td>
<td>2018</td>
</tr>
<tr>
<td>PLDI, Program Committee</td>
<td>2018</td>
</tr>
<tr>
<td>Onward!, <strong>Program Chair</strong></td>
<td>2017</td>
</tr>
<tr>
<td>CAV, Program Committee</td>
<td>2017</td>
</tr>
<tr>
<td>ICSE Visions of 2025 and Beyond, Program Committee</td>
<td>2016</td>
</tr>
<tr>
<td>SYNT, Program Committee</td>
<td>2016</td>
</tr>
<tr>
<td>Onward!, Program Committee</td>
<td>2016</td>
</tr>
<tr>
<td>POPL, Program Committee</td>
<td>2016</td>
</tr>
<tr>
<td>CAV, Program Committee</td>
<td>2015</td>
</tr>
<tr>
<td>RV, Program Committee</td>
<td>2015</td>
</tr>
<tr>
<td>SNAPL, Program Committee</td>
<td>2015</td>
</tr>
<tr>
<td>POPL, External Review Committee</td>
<td>2015</td>
</tr>
<tr>
<td>ICSE, Review Committee</td>
<td>2015</td>
</tr>
<tr>
<td>GPCE, Program Committee</td>
<td>2014</td>
</tr>
<tr>
<td>DSLDI, Program Committee</td>
<td>2014</td>
</tr>
<tr>
<td>SYNT, Program Committee</td>
<td>2014</td>
</tr>
<tr>
<td>CSTVA, Program Committee</td>
<td>2014</td>
</tr>
<tr>
<td>POPL OBT, Program Committee</td>
<td>2014</td>
</tr>
<tr>
<td>OOPSLA, External Review Committee</td>
<td>2014</td>
</tr>
<tr>
<td>PLDI, External Review Committee</td>
<td>2013</td>
</tr>
<tr>
<td>PLDI Student Research Competition, Program Committee</td>
<td>2013</td>
</tr>
<tr>
<td>SPLASH Posters, Program Co-Chair</td>
<td>2013</td>
</tr>
<tr>
<td>PLDI, Program Committee</td>
<td>2012</td>
</tr>
<tr>
<td>OOPSLA, Program Committee</td>
<td>2012</td>
</tr>
<tr>
<td>LaSh, Program Committee</td>
<td>2010</td>
</tr>
<tr>
<td>IBM Programming Languages Day, Program Chair</td>
<td>2010</td>
</tr>
</table>
<h2 id="Students">Students</h2>
<table>
<tr>
<td><a href="https://homes.cs.washington.edu/~sorawee/">Sorawee Porncharoenwase</a>, Ph.D.</td>
<td>2023</td>
</tr>
<tr>
<td><a href="https://homes.cs.washington.edu/~jsvg/">Jacob Van Geffen</a>, Ph.D.</td>
<td>2023</td>
</tr>
<tr>
<td><a href="https://www.cs.utexas.edu/~bornholt/">James Bornholt</a>, Ph.D.</td>
<td>2019</td>
</tr>
<tr>
<td><a href="https://www.ericbutler.net/">Eric Butler</a>, Ph.D.</td>
<td>2018</td>
</tr>
<tr>
<td>Vimala Jampala, M.Sc.</td>
<td>2015</td>
</tr>
</table>
<h2 id="Teaching">Teaching</h2>
<table>
<tr>
<td><a href="https://courses.cs.washington.edu/courses/cse507/21au/">CSE 507: Computer-Aided Reasoning for Software</a></td>
<td>2014–2021</td>
</tr>
<tr>
<td><a href="https://courses.cs.washington.edu/courses/cse311/20sp/">CSE 311: Foundations of Computing I</a></td>
<td>2018–2020</td>
</tr>
<tr>
<td><a href="https://courses.cs.washington.edu/courses/cse403/">CSE 403: Software Engineering</a></td>
<td>2015–2016</td>
</tr>
<tr>
<td><a href="https://courses.cs.washington.edu/courses/cse599a2/15wi/">CSE 599 A2: Advanced Computer-Aided Reasoning for Software</a></td>
<td>2015</td>
</tr>
<tr>
<td><a href="https://homes.cs.washington.edu/~bodik/ucb/cs294fa12.html">CS294: Program Synthesis for Everyone</a></td>
<td>2012</td>
</tr>
</table>
<footer>© Emina Torlak. All rights reserved. Built with <a href="https://docs.racket-lang.org/pollen/">Pollen</a>. Last updated 6 Jan 2025.</footer>
</body>
</html>