Emina Torlak


My research aims to help people create better software more easily. As part of this agenda, I develop new languages and tools for computer-aided design, verification, and synthesis of software. My collaborators and I apply these techniques to all kinds of systems, from radiotherapy machines to automated algebra tutors. A lot of our work is based on Rosette, a new language that makes it easy to create efficient tools for program verification, synthesis, and more.

Jul 22 Gave the Junior DN Prize Lecture at ECOOP’16.
Mar 25 Released Rosette 2.0: new theories, better performance!
Feb 28 Received a Sloan Research Fellowship.
Jan 20 Won the AITO Dahl-Nygaard Junior Prize.

Recent Publications

All Publications DBLP Google Scholar
  • [1] 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. (DOI, PDF, Web)
  • [2] Eric Butler, Emina Torlak, and Zoran Popovic. A Framework for Parameterized Design of Rule Systems Applied to Algebra. Intelligent Tutoring Systems (ITS), 2016. (DOI, PDF)
  • [3] Calvin Loncaric, Emina Torlak, and Michael D. Ernst. Fast synthesis of fast collections. Programming Language Design and Implementation (PLDI), 2016. (DOI, PDF, Web)
  • [4] 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. (DOI, PDF, Web)
  • [5] James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. Principles of Programming Languages (POPL), 2016. (DOI, PDF, Web)
  • [6] 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 and Software (Onward!), 2015. (DOI, PDF)
  • [7] John Toman, Stuart Pernsteiner, and Emina Torlak. CRust: A Bounded Verifier for Rust. Automated Software Engineering (ASE), 2015. (PDF, Web)
  • [8] 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. (DOI, PDF, Web)
  • [9] 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. (DOI, PDF)
  • [10] Emina Torlak and Rastislav Bodik. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. Programming Language Design and Implementation (PLDI), 2014. (DOI, PDF, Web)