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.

Sep 18 Gave the keynote at RacketCon’16.
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] 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. (DOI, PDF, Web)
  • [2] Pavel Panchekha and Emina Torlak. Automated Reasoning for Web Page Layout. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. (DOI, PDF, Web)
  • [3] 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. (DOI, PDF, Web)
  • [4] 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)
  • [5] 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)
  • [6] Calvin Loncaric, Emina Torlak, and Michael D. Ernst. Fast synthesis of fast collections. Programming Language Design and Implementation (PLDI), 2016. (DOI, PDF, Web)
  • [7] 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)
  • [8] James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. Principles of Programming Languages (POPL), 2016. (DOI, PDF, Web)
  • [9] 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)
  • [10] John Toman, Stuart Pernsteiner, and Emina Torlak. CRust: A Bounded Verifier for Rust. Automated Software Engineering (ASE), 2015. (PDF, Web)