Emina Torlak: CV

Research Interests

Tools and languages for computer-aided design, verification, and synthesis of software.

Education

Massachusetts Institute of Technology, Ph.D., Computer Science Thesis: A Constraint Solver for Software Engineering Advisor: Daniel Jackson	2009
Massachusetts Institute of Technology, M.Eng., Computer Science Thesis: Subtyping in Alloy Advisor: Daniel Jackson	2004
Massachusetts Institute of Technology, B.Sc., Computer Science	2003

Employment

Amazon Web Services, Seattle, WA Senior Principal Scientist	2021-present
University of Washington, Seattle, WA Associate Professor, Paul G. Allen School of Computer Science & Engineering	2018-present
University of Washington, Seattle, WA Assistant Professor, Paul G. Allen School of Computer Science & Engineering	2014-2018
University of California Berkeley, Berkeley, CA Researcher, Electrical Engineering and Computer Sciences	2012-2014
LogicBlox, Inc., Atlanta, GA Senior Computer Scientist, Compiler Technologies Group	2011
IBM Research, Hawthorne, NY Research Staff Member, Programming Technologies Department	2008-2010

Awards

Robin Milner Young Researcher Award	2021
Amazon Research Award	2020
Distinguished Paper Award for [3]	2020
Best Paper and Distinguished Artifact Awards for [6]	2019
Distinguished Paper Award for [10]	2018
Distinguished Artifact Award for [8]	2018
NSF CAREER Award	2017
Sloan Research Fellow	2016
Best Paper Award for [19]	2016
The AITO Dahl-Nygaard Junior Prize	2016
Distinguished Paper Award for [35]	2012

Publications

Conference Papers

[1] Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak. A formal foundation for symbolic evaluation with merging. Principles of Programming Languages (POPL), 2022.
[2] Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. Operating Systems Design and Implementation (OSDI), 2020.
[3] Yu Feng, Emina Torlak, and Rastislav Bodik. Summary-Based Symbolic Evaluation for Smart Contracts. Automated Software Engineering (ASE), 2020. Distinguished Paper Award.
[4] Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak. Synthesizing JIT Compilers for In-Kernel DSLs. Computer Aided Verification (CAV), 2020.
[5] Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. Fixing Code That Explodes Under Symbolic Evaluation. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2020.
[6] Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. Symposium on Operating Systems Principles (SOSP), 2019. Best Paper and Distinguished Artifact Awards.
[7] Phitchaya Mangpo Phothilimthana, Archibald Samuel Elliott, An Wang, Abhinav Jangda, Bastian Hagedorn, Henrik Barthels, Samuel J. Kaufman, Vinod Grover, Emina Torlak, and Rastislav Bodik. Swizzle Inventor: Data Movement Synthesis for GPU Kernels. Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2019.
[8] James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2018. Distinguished Artifact Award.
[9] Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A Framework for Design and Verification of Information Flow Control Systems. Operating Systems Design and Implementation (OSDI), 2018.
[10] Calvin Loncaric, Michael D. Ernst, and Emina Torlak. Generalized Data Structure Synthesis. International Conference on Software Engineering (ICSE), 2018. Distinguished Paper Award.
[11] Eric Butler, Emina Torlak, and Zoran Popovic. A Framework for Computer-Aided Design of Educational Domain Models. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2018.
[12] Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeff Foster, and Emina Torlak. Refinement Types for Ruby. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2018.
[13] Stephen Chang, Alex Knauth, and Emina Torlak. Symbolic Types for Lenient Symbolic Execution. Principles of Programming Languages (POPL), 2018.
[14] Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, and Emina Torlak. Automatic Formal Verification for EPICS. International Conference on Accelerator and Large Experimental Control Systems (ICALEPCS), 2017.
[15] Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. Symposium on Operating Systems Principles (SOSP), 2017.
[16] Eric Butler, Emina Torlak, and Zoran Popovic. Synthesizing Interpretable Strategies for Solving Puzzle Games. Foundations of Digital Games (FDG), 2017.
[17] James Bornholt and Emina Torlak. Synthesizing Memory Models from Framework Sketches and Litmus Tests. Programming Language Design and Implementation (PLDI), 2017.
[18] Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock. SpaceSearch: A Library for Building and Verifying Solver-Aided Tools. International Conference on Functional Programming (ICFP), 2017.
[19] Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. Operating Systems Design and Implementation (OSDI), 2016. Best Paper Award.
[20] Pavel Panchekha and Emina Torlak. Automated Reasoning for Web Page Layout. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016.
[21] Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016.
[22] Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky. Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. Computer-Aided Verification (CAV), 2016.
[23] Eric Butler, Emina Torlak, and Zoran Popovic. A Framework for Parameterized Design of Rule Systems Applied to Algebra. Intelligent Tutoring Systems (ITS), 2016.
[24] Calvin Loncaric, Emina Torlak, and Michael D. Ernst. Fast synthesis of fast collections. Programming Language Design and Implementation (PLDI), 2016.
[25] James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Specifying and Checking File System Crash-Consistency Models. Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016.
[26] James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. Principles of Programming Languages (POPL), 2016.
[27] Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler. Toward Tool Support for Interactive Synthesis. New Ideas, New Paradigms, and Reflections on Programming & Software (Onward!), 2015.
[28] John Toman, Stuart Pernsteiner, and Emina Torlak. CRust: A Bounded Verifier for Rust. Automated Software Engineering (ASE), 2015.
[29] Michael Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang. Toward a Dependability Case Language and Workflow for a Radiation Therapy System. Summit on Advances in Programming Languages (SNAPL), 2015.
[30] Emina Torlak and Rastislav Bodik. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. Programming Language Design and Implementation (PLDI), 2014.
[31] Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, and Satish Chandra. What Gives?: A Hybrid Algorithm for Error Trace Explanation. Verified Software: Theories, Tools and Experiments (VSTTE), 2014.
[32] Emina Torlak and Rastislav Bodik. Growing Solver-Aided Languages with Rosette. New Ideas, New Paradigms, and Reflections on Programming & Software (Onward!), 2013.
[33] 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. Syntax-Guided Synthesis. Formal Methods in Computer-Aided Design (FMCAD), 2013.
[34] Rastislav Bodik and Emina Torlak. Synthesizing Programs with Constraint Solvers (Invited Tutorial). Computer Aided Verification (CAV), 2012.
[35] Emina Torlak. Scalable test data generation from multidimensional models. Foundations of Software Engineering (FSE), 2012. Distinguished Paper Award.
[36] Satish Chandra, Emina Torlak, Shaon Barman, and Rastislav Bodik. Angelic Debugging. International Conference on Software Engineering (ICSE), 2011.
[37] Max Schaefer, Julian Dolby, Manu Sridharan, Emina Torlak, and Frank Tip. Correct Refactoring of Concurrent Java Code. European Conference on Object-Oriented Programming (ECOOP), 2010.
[38] Emina Torlak, Mandana Vaziri, and Julian Dolby. MemSAT: Checking Axiomatic Specifications of Memory Models. Programming Language Design and Implementation (PLDI), 2010.
[39] Emina Torlak, and Satish Chandra. Effective interprocedural resource leak detection. International Conference on Software Engineering (ICSE), 2010.
[40] Emina Torlak, Felix Sheng-Ho Chang, and Daniel Jackson. Finding Minimal Unsatisfiable Cores of Declarative Specifications. Formal Methods (FM), 2008.
[41] Emina Torlak and Daniel Jackson. Kodkod: A Relational Model Finder. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
[42] Jonathan Edwards, Daniel Jackson, Emina Torlak, and Vincent Yeung. Faster constraint solving with subtypes. International Symposium on Software Testing and Analysis (ISSTA), 2004.
[43] Jonathan Edwards, Daniel Jackson, and Emina Torlak. A type system for object models. Foundations of Software Engineering (FSE), 2004.

Journal Papers

[44] Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review, 2020.
[45] 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. Syntax-Guided Synthesis. Dependable Software Systems Engineering, 2015.
[46] Emina Torlak, Mana Taghdiri, Greg Dennis, and Joseph Near. Applications and Extensions of Alloy: Past, Present, and Future. (Invited Paper). Mathematical Structures in Computer Science (MSCS), 2013.
[47] Blaise Gassend, Marten Van Dijk, Dwaine Clarke, Emina Torlak, Srinivas Devadas, and Pim Tuyls. Controlled physical random functions and applications. ACM Transactions on Information and System Security (TISSEC), 2008.

Workshop Papers

[48] Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Formal Semantics and Automated Verification for the Border Gateway Protocol. ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL), 2016.
[49] James Bornholt and Emina Torlak. Scaling program synthesis by exploiting existing code. Machine Learning for Programming Languages Workshop (ML4PL), 2015.
[50] James Bornholt, Emina Torlak, Luis Ceze, and Dan Grossman. Approximate Program Synthesis. Workshop on Approximate Computing Across the Stack (WAX), 2015.
[51] Emina Torlak and Greg Dennis. Kodkod for Alloy Users. Alloy Workshop, 2006.

Technical Reports

[52] Eric Butler, Emina Torlak, and Zoran Popovic. Synthesizing Optimal Domain Models for Educational Applications. University of Washington Computer Science & Engineering, 2017.
[53] Konstantin Weitz, Dough Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Bagpipe: Verified BGP Configuration Checking. University of Washington Computer Science & Engineering, 2016.
[54] Emina Torlak. Scalable Test Data Generation from Multidimensional Models. University of California, Berkeley, 2012.
[55] Shaon Barman, Ras Bodik, Satish Chandra, and Emina Torlak. Discovering Algorithms in Angelic Programs. IBM Research, 2010.
[56] Emina Torlak and Daniel Jackson. The Design of a Relational Engine. Massachusetts Institute of Technology, 2006.
[57] Marten van Dijk, Emina Torlak, Blaise Gassend, and Srinivas Devadas. A Generalized Two-Phase Analysis of Knowledge Flows in Security Protocols. arXiv.org, 2006.
[58] Emina Torlak, Marten van Dijk, Blaise Gassend, Daniel Jackson, and Srinivas Devadas. Knowledge Flow Analysis for Security Protocols. arXiv.org, 2006.

Theses

[59] Emina Torlak. A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. Massachusetts Institute of Technology, 2009.
[60] Emina Torlak. Subtyping in Alloy. Massachusetts Institute of Technology, 2004.

Patents

[61] Shaon K. Barman, Satish Chandra, and Emina Torlak. Precise fault localization. U.S. Patent Application No. 13/006,126, Publication No. US 2012/0185731 A1, 2012.
[62] Julian Dolby, Max Schaefer, Manu Sridharan, Frank Tip, and Emina Torlak. Correct Refactoring of Concurrent Software. U.S. Patent Application No. 12/718,648, Publication No. US 2011/0219361 A1, 2011.
[63] Julian Dolby, Emina Torlak, and Mandana Vaziri. System and Method for Debugging Memory Consistency Models. U.S. Patent Application No. 12/615,657, Publication No. US 2011/0113285 A1, 2011.
[64] Satish Chandra, and Emina Torlak. Systems and Methods for Resource Leak Detection. U.S. Patent Application No. 12/611,561, Publication No. US 2011/0107297 A1, 2011.

Grants

FMitF: A Framework for Synthesis of Efficient, Reliable, and Secure Operating System Components Co-PI, NSF CCF-1836724, $980,043	2018-2022
CAREER: The Next 700 Solver-Aided Languages PI, NSF CCF-1651225, $498,577	2017-2022
ARION: Taming Heterogeneity with DSLs, Approximation, and Synthesis Co-PI, NSF CCF-1723352, $850,000	2017-2020
A Picture is Worth a Billion Bits: Adaptive Visualization of Big Data Co-PI, DARPA, $7,500,000	2015-2018
General-Purpose Approximate Computing Across the System Stack Co-PI, NSF CCF-1518703, $2,400,000	2015-2020
Automated Probabilistic Programming Representation and Inference Languages Co-PI, DARPA, $1,369,735	2013-2017
XPS: FP: Program Synthesis for Low-Power Spatial Architectures Co-PI, NSF CCF-1337415, $749,877	2013-2016
DSL Technology for Exascale Computing (D-TEC) Key Personnel, DOE DE-SC0008923, $11,605,314	2012-2015
Computed Aided Development for Mobile Applications Co-PI, Samsung Electronics, $126,086	2012-2013
Software Synthesis for High Productivity Exascale Computing Co-PI, DOE DE-SC0005136, $683,344	2012-2013

Presentations and Seminars

Solver-Aided Programming for All
Programming Language Design and Implementation (PLDI), Invited Talk	Jun 2021
Northwestern University, Invited Talk	Apr 2021
Amazon, Invited Talk	Apr 2021
UMass Amherst, Invited Talk	Feb 2021
University of Iowa, Invited Talk	Oct 2020
Facebook PLEMM, Invited Talk	Sep 2019
International Conference on Functional Programming (ICFP), Keynote	Aug 2019
EPFL, Invited Talk	Aug 2019
International Symposium on Software Testing and Analysis (ISSTA), Keynote	Jul 2018

Solver-aided verification for systems software
Newton Institute Workshop on Verified Software, Invited talk	Jun 2021

A Unified Framework for Reasoning about Critical Infrastructure Software
Algorand, Invited Talk, joint with Xi Wang	Mar 2021
Intel, Invited Talk, joint with Xi Wang	Oct 2020

Solver-Aided Programming
Computer-Aided Verification (CAV), Invited Tutorial	Jul 2019
Summer School on Formal Techniques (SSFT), Invited Tutorial	May 2018

Finding Code That Explodes Under Symbolic Evaluation
IFIP Working Group 2.3, Invited Talk	May 2018

Synthesis and Verification for All
Clojure/West, Keynote	Mar 2017
DARPA ISAT Augmented Developers Workshop, Invited Talk	Feb 2017
RacketCon, Keynote	Sep 2016
European Conference on Object-Oriented Programming (ECOOP), Junior DN Prize Lecture	Jul 2016

Optimizing Synthesis with Metasketches
IFIP Working Group 2.4, Invited Talk	Apr 2016
IFIP Working Group 2.3, Invited Talk	Jan 2016

Synthesis and Verification for Everyone
Cornell University, Invited Seminar	Sep 2015
European Conference on Object-Oriented Programming (ECOOP), Invited Talk	Jul 2015

Formal, Machine-Checkable Dependability Cases for End-to-End Safety Properties
IFIP Working Group 2.4, Invited Talk	Jul 2015
Summit on Advances in Programming Languages (SNAPL), Conference Talk	May 2015
IFIP Working Group 2.3, Invited Talk	Mar 2015

Programming for Everyone: Languages That Automate Coding, Verification, and Debugging
TTI/Vanguard, Invited Talk	Sep 2014

Programming for Everyone: From Solvers to Solver-Aided Languages and Beyond
Stanford University, Stanford Software Seminar	Jul 2014
Summer School on Formal Techniques (SSFT), Invited Talk	May 2014
University of Washington, Invited Seminar	May 2014
Samsung Electronics, Invited Seminar	Apr 2014
University of Texas at Austin, ECE, Invited Seminar	Apr 2014
University of Pennsylvania, Invited Seminar	Apr 2014
Princeton University, Invited Seminar	Mar 2014
University of Southern California, Invited Seminar	Mar 2014
Microsoft Research, Redmond, Invited Seminar	Mar 2014
University of Wisconsin-Madison, Invited Seminar	Mar 2014
Purdue University, Invited Seminar	Feb 2014
University of California, Berkeley, Invited Seminar	Feb 2014
Northeastern University, Invited Seminar	Feb 2014
IBM T. J. Watson Research Center, Invited Seminar	Jan 2014
University of California, Los Angeles, Invited Seminar	Jan 2014

A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages
Programming Language Design and Implementation (PLDI), Conference Talk	Jun 2014
IFIP Working Group 2.4, Invited Talk	Feb 2014

Growing Solver-Aided Languages with Rosette
Kestrel Institute, Invited Seminar	Dec 2013
Viewpoints Research Institute, Invited Seminar	Dec 2013
New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), Conference Talk	Oct 2013
IFIP Working Group 2.3, Invited Talk	Jun 2013
Northeastern University, Invited Seminar	Apr 2013
Dagstuhl Seminar 13061 (Fault Prediction, Localization, and Repair), Invited Talk	Feb 2013

Synthesizing Programs with Constraint Solvers
Expeditions in Computer Augmented Program Engineering (ExCAPE) Summer School, Invited Lecture Series (with Rastislav Bodik)	Jun 2013
Computer-Aided Verification (CAV), Invited Tutorial (with Rastislav Bodik)	Jul 2012

Programming with Constraint Solvers: Toward a Shared Infrastructure for Code Checking, Angelic Execution, Debugging, and Synthesis
Georgia Institute of Technology, Invited Seminar	Nov 2012
SRI International, Invited Seminar	Sep 2012
Workshop on Intermediate Verification Languages (Boogie), Invited Talk	Jul 2012

Scalable Test Data Generation from Multidimensional Models
Foundations of Software Engineering (FSE), Conference Talk	Nov 2012
IFIP Working Group 2.4, Invited Talk	May 2012
University of California, Berkeley (ParLab), Invited Seminar	Aug 2011

Kodkod by Example: Code Checking, Data Repair, Debugging and Synthesis
Dagstuhl Seminar 12152 (Software Synthesis), Invited Tutorial	Apr 2012

MemSAT: Checking Axiomatic Specifications of Memory Models
First International SAT/SMT Summer School, Invited Lecture	Jun 2011
Purdue University (Secure Software Systems), Invited Seminar	Sep 2011
Programming Language Design and Implementation (PLDI), Conference Talk	Jun 2010
University of California, Berkeley (ParLab), Invited Seminar	Oct 2009

Effective Interprocedural Resource Leak Detection
International Conference on Software Engineering (ICSE), Conference Talk	May 2010

Finding Minimal Unsatisfiable Cores of Declarative Specifications
Formal Methods (FM), Conference Talk	May 2008

Kodkod: A Constraint Solver for Relational Logic
International Workshop on Logic and Search (LaSh), Invited Talk	Jul 2010
IBM Research (Hawthorne), Invited Seminar	Apr 2008
Microsoft Research (Redmond), Invited Seminar	Apr 2008
NASA JPL (Lab for Reliable Software), Invited Seminar	Nov 2007
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Conference Talk	Mar 2007

Professional Service and Activities

Professional Societies

IFIP Working Group 2.3: Programming Methodology, Member	2016-present
IFIP Working Group 2.4: Software Implementation Technology, Member	2015-2018

Conference and Workshop Organization

Programming Language Design and Implementation (PLDI), Program Chair	2020
The Future of Alloy Workshop, Program Co-Chair	2018
New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), Program Chair	2017
SPLASH Posters, Track Co-Chair	2013
IBM Programming Languages Day, Program Chair	2010

Steering Committees

New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), SC	2018
Programming Language Design and Implementation (PLDI), SC Member at Large	2018

Program Committees, Review Committees, and External Review Committees

Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), RC	2019
Programming Language Design and Implementation (PLDI), PC	2019
Programming Language Design and Implementation (PLDI), PC	2018
Computer-Aided Verification (CAV), PC	2017
Principles of Programming Languages (POPL), PC	2016
Workshop on Synthesis (SYNT), PC	2016
New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), PC	2016
Visions of 2025 and Beyond (V2025) at ICSE 2016, PC	2016
Summit on Advances in Programming Languages (SNAPL), PC	2015
Runtime Verification (RV), PC	2015
Computer-Aided Verification (CAV), PC	2015
International Conference on Software Engineering (ICSE), RC	2015
Principles of Programming Languages (POPL), ERC	2015
Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), ERC	2014
Principles of Programming Languages Off-the-Beaten Track (POPL OBT), PC	2014
Constraints in Software Testing, Verification and Analysis (CSTVA), PC	2014
Domain-Specific Language Design and Implementation (DSLDI), PC	2014
Generative Programming: Concepts & Experiences (GPCE), PC	2014
Workshop on Synthesis (SYNT), PC	2014
Programming Language Design and Implementation (PLDI), ERC	2013
PLDI Student Research Competition, PC	2013
Programming Language Design and Implementation (PLDI), PC	2012
Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), PC	2012
International Workshop on Logic and Search (LaSh), PC	2010

Refereeing and Reviewing

ACM Transactions on Software Engineering and Methodology (TOSEM)	2012
Mathematical Structures in Computer Science (MSCS)	2011
Science of Computer Programming	2010
International Conference on Software Engineering (ICSE)	2010
European Symposium on Programming (ESOP)	2010

Students

Sorawee Porncharoenwase, PhD
Jacob Van Geffen, PhD
James Bornholt, PhD	2019
Eric Butler, PhD	2018
Vimala Jampala, MS	2015

Teaching

CSE 507: Computer-Aided Reasoning for Software	2014-2021
CSE 311: Foundations of Computing I	2018-2020
CSE 403: Software Engineering	2015-2016
CSE 599 A2: Advanced Computer-Aided Reasoning for Software	2015
CS294: Program Synthesis for Everyone	2012