Emina Torlak

https://emina.github.io/

Education

Massachusetts Institute of Technology, Ph.D., Computer Science 2009
Massachusetts Institute of Technology, M.Eng., Computer Science 2004
Massachusetts Institute of Technology, B.Sc., Computer Science 2003

Employment

Senior Principal Applied Scientist, Amazon Web Services 2021–
Affiliate Professor, Allen School, University of Washington 2024–
Associate Professor, Allen School, University of Washington 2018–2023
Assistant Professor, Allen School, University of Washington 2014–2018
Research Engineer, EECS, University of California Berkeley 2012–2014
Senior Computer Scientist, LogicBlox, Inc. 2011
Research Staff Member, IBM Research 2008–2010

Awards

ICSE Distinguished Paper Award [1] 2025
Robin Milner Young Researcher Award 2021
Amazon Research Award 2020
ASE Distinguished Paper Award [10] 2020
SOSP Best Paper and Distinguished Artifact Awards [13] 2019
OOPSLA Distinguished Artifact Award [15] 2018
ICSE Distinguished Paper Award [17] 2018
NSF CAREER Award 2017
Sloan Research Fellow 2016
The AITO Dahl-Nygaard Junior Prize 2016
OSDI Best Paper Award [26] 2016
FSE Distinguished Paper Award [44] 2012

Publications

Conference and Journal Papers

  1. Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Samuel Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clement Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas Wagner, Michael Whalen, Remy Willems, Tongtong Xiang, Taejoon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, and Yongwei Yuan. Formally Verified Cloud-Scale Authorization. ICSE, 2025. Distinguished Paper Award.
  2. 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. How We Built Cedar: A Verification-Guided Approach. FSE, 2024.
  3. 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. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. OOPSLA, 2024.
  4. Sorawee Porncharoenwase, Justin Pombrio, and Emina Torlak. A pretty expressive printer. OOPSLA, 2023.
  5. Jacob Van Geffen, Xi Wang, Emina Torlak, and James Bornholt. Synthesis-Aided Crash Consistency for Storage Systems. ECOOP, 2023.
  6. Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, and Emina Torlak. Testing Dafny (experience paper). ISSTA, 2022.
  7. Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak. A formal foundation for symbolic evaluation with merging. POPL, 2022.
  8. 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. OSDI, 2020.
  9. Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review, 2020.
  10. Yu Feng, Emina Torlak, and Rastislav Bodik. Summary-Based Symbolic Evaluation for Smart Contracts. ASE, 2020. Distinguished Paper Award.
  11. Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak. Synthesizing JIT Compilers for In-Kernel DSLs. CAV, 2020.
  12. Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. Fixing Code That Explodes Under Symbolic Evaluation. VMCAI, 2020.
  13. Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. SOSP, 2019. Best Paper and Distinguished Artifact Awards.
  14. 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. ASPLOS, 2019.
  15. James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. OOPSLA, 2018. Distinguished Artifact Award.
  16. 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. OSDI, 2018.
  17. Calvin Loncaric, Michael D. Ernst, and Emina Torlak. Generalized Data Structure Synthesis. ICSE, 2018. Distinguished Paper Award.
  18. Eric Butler, Emina Torlak, and Zoran Popovic. A Framework for Computer-Aided Design of Educational Domain Models. VMCAI, 2018.
  19. Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeff Foster, and Emina Torlak. Refinement Types for Ruby. VMCAI, 2018.
  20. Stephen Chang, Alex Knauth, and Emina Torlak. Symbolic Types for Lenient Symbolic Execution. POPL, 2018.
  21. Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, and Emina Torlak. Automatic Formal Verification for EPICS. ICALEPCS, 2017.
  22. Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. SOSP, 2017.
  23. Eric Butler, Emina Torlak, and Zoran Popovic. Synthesizing Interpretable Strategies for Solving Puzzle Games. FDG, 2017.
  24. James Bornholt and Emina Torlak. Synthesizing Memory Models from Framework Sketches and Litmus Tests. PLDI, 2017.
  25. Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock. SpaceSearch: A Library for Building and Verifying Solver-Aided Tools. ICFP, 2017.
  26. Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. OSDI, 2016. Best Paper Award.
  27. Pavel Panchekha and Emina Torlak. Automated Reasoning for Web Page Layout. OOPSLA, 2016.
  28. 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. OOPSLA, 2016.
  29. 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. CAV, 2016.
  30. Eric Butler, Emina Torlak, and Zoran Popovic. A Framework for Parameterized Design of Rule Systems Applied to Algebra. ITS, 2016.
  31. Calvin Loncaric, Emina Torlak, and Michael D. Ernst. Fast synthesis of fast collections. PLDI, 2016.
  32. James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Specifying and Checking File System Crash-Consistency Models. ASPLOS, 2016.
  33. James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. POPL, 2016.
  34. Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler. Toward Tool Support for Interactive Synthesis. Onward!, 2015.
  35. John Toman, Stuart Pernsteiner, and Emina Torlak. CRust: A Bounded Verifier for Rust. ASE, 2015.
  36. 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. SNAPL, 2015.
  37. 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.
  38. Emina Torlak and Rastislav Bodik. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. PLDI, 2014.
  39. Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, and Satish Chandra. What Gives?: A Hybrid Algorithm for Error Trace Explanation. VSTTE, 2014.
  40. Emina Torlak and Rastislav Bodik. Growing Solver-Aided Languages with Rosette. Onward!, 2013.
  41. 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. FMCAD, 2013.
  42. Emina Torlak, Mana Taghdiri, Greg Dennis, and Joseph Near. Applications and Extensions of Alloy: Past, Present, and Future. Mathematical Structures in Computer Science, 2013.
  43. Rastislav Bodik and Emina Torlak. Synthesizing Programs with Constraint Solvers (Invited Tutorial). CAV, 2012.
  44. Emina Torlak. Scalable test data generation from multidimensional models. FSE, 2012. Distinguished Paper Award.
  45. Satish Chandra, Emina Torlak, Shaon Barman, and Rastislav Bodik. Angelic Debugging. ICSE, 2011.
  46. Max Schaefer, Julian Dolby, Manu Sridharan, Emina Torlak, and Frank Tip. Correct Refactoring of Concurrent Java Code. ECOOP, 2010.
  47. Emina Torlak, Mandana Vaziri, and Julian Dolby. MemSAT: Checking Axiomatic Specifications of Memory Models. PLDI, 2010.
  48. Emina Torlak and Satish Chandra. Effective interprocedural resource leak detection. ICSE, 2010.
  49. Emina Torlak, Felix Sheng-Ho Chang, and Daniel Jackson. Finding Minimal Unsatisfiable Cores of Declarative Specifications. FM, 2008.
  50. 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, 2008.
  51. Emina Torlak and Daniel Jackson. Kodkod: A Relational Model Finder. TACAS, 2007.
  52. Jonathan Edwards, Daniel Jackson, Emina Torlak, and Vincent Yeung. Faster constraint solving with subtypes. ISSTA, 2004.
  53. Jonathan Edwards, Daniel Jackson, and Emina Torlak. A type system for object models. FSE, 2004.

Patents and Theses

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. Emina Torlak. A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. Ph.D. thesis, MIT, 2009.
  6. Emina Torlak. Subtyping in Alloy. Masters thesis, MIT, 2004.

Service

PLDI, Area Chair 2024
The Dahl–Nygaard Prize Committee, Member 2024
POPL, Associate Chair 2024
PLDI, Steering Committee 2018–2023
PLDI, Program Chair 2020
SPLASH, Steering Committee 2018–2020
PLDI, Program Committee 2019
OOPSLA, Review Committee 2019
The Future of Alloy Workshop, Program Co-Chair 2018
PLDI, Program Committee 2018
Onward!, Program Chair 2017
CAV, Program Committee 2017
ICSE Visions of 2025 and Beyond, Program Committee 2016
SYNT, Program Committee 2016
Onward!, Program Committee 2016
POPL, Program Committee 2016
CAV, Program Committee 2015
RV, Program Committee 2015
SNAPL, Program Committee 2015
POPL, External Review Committee 2015
ICSE, Review Committee 2015
GPCE, Program Committee 2014
DSLDI, Program Committee 2014
SYNT, Program Committee 2014
CSTVA, Program Committee 2014
POPL OBT, Program Committee 2014
OOPSLA, External Review Committee 2014
PLDI, External Review Committee 2013
PLDI Student Research Competition, Program Committee 2013
SPLASH Posters, Program Co-Chair 2013
PLDI, Program Committee 2012
OOPSLA, Program Committee 2012
LaSh, Program Committee 2010
IBM Programming Languages Day, Program Chair 2010

Students

Sorawee Porncharoenwase, Ph.D. 2023
Jacob Van Geffen, Ph.D. 2023
James Bornholt, Ph.D. 2019
Eric Butler, Ph.D. 2018
Vimala Jampala, M.Sc. 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